rng (a * f) c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (a * f) or x in NAT )
assume x in rng (a * f) ; :: thesis: x in NAT
then ex xx being object st
( xx in dom (a * f) & x = (a * f) . xx ) by FUNCT_1:def 3;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

hence a (#) f is FinSequence of NAT by FINSEQ_1:def 4; :: thesis: verum