let f be NAT * -defined to-naturals homogeneous len-total Function; :: thesis: f is quasi_total Element of HFuncs NAT
reconsider f' = f as Element of HFuncs NAT by Th31;
f' is quasi_total

proof

let x, y be FinSequence of NAT ; :: according to UNIALG_1:def 2 :: thesis: ( not len x = len y or not x in dom f' or y in dom f' )
assume that
A1: len x = len y and
A2: x in dom f' ; :: thesis: y in dom f'
thus y in dom f' by A1, A2, Def3; :: thesis: verum

end;

hence f is quasi_total Element of HFuncs NAT ; :: thesis: verum