let g be NAT * -defined to-naturals len-total Function; :: thesis: g is quasi_total PartFunc of ,
A1: rng g c= NAT by VALUED_0:def 6;
dom g c= NAT * by RELAT_1:def 18;
then reconsider g' = g as PartFunc of , 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 , ; :: thesis: verum