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 consider xx being object such that
A1: xx in dom (a * f) and
A2: x = (a * f) . xx by FUNCT_1:def 3;
reconsider xx = xx as Element of NAT by A1;
(a * f) . xx = a * (f . xx) by RVSUM_1:44;
hence x in NAT by A2, ORDINAL1:def 12; :: thesis: verum

end;

hence a * f is FinSequence of NAT by FINSEQ_1:def 4; :: thesis: verum