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 ( len x = len y & x in dom f' ) ; :: thesis: y in dom f'
hence y in dom f' by Def3; :: thesis: verum

end;

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