Description: T is an onto function. (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 13-Feb-2022) (Revised by AV, 31-Oct-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | extwwlkfab.v | |
|
extwwlkfab.c | |
||
extwwlkfab.f | |
||
numclwwlk.t | |
||
Assertion | numclwwlk1lem2fo | |