let f be NAT * -defined to-naturals homogeneous len-total Function; :: thesis: f is quasi_total Element of HFuncs NAT
reconsider f9 = f as Element of HFuncs NAT by Th31;
f9 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 proj1 f9 or y in proj1 f9 )
assume that
A1: len x = len y and
A2: x in dom f9 ; :: thesis: y in proj1 f9
thus y in dom f9 by A1, A2, Def3; :: thesis: verum

end;

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