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