theorem Th28: :: COMPUT_1:29

for f being NAT * -defined to-naturals homogeneous len-total Function holds f is quasi_total Element of HFuncs NAT