let g be NAT * -defined to-naturals len-total Function; :: thesis: g is quasi_total PartFunc of (NAT *),NAT
A1: rng g c= NAT by VALUED_0:def 6;
dom g c= NAT * ;
then reconsider g9 = g as PartFunc of (NAT *),NAT by A1, RELSET_1:4;
for x, y being FinSequence of NAT st len x = len y & x in dom g holds
y in dom g by Def2;
then g9 is quasi_total ;
hence g is quasi_total PartFunc of (NAT *),NAT ; :: thesis: verum