rng (a * f) c= NAT

proof

let x be set ; :: 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 set such that
A1: xx in dom (a * f) and
A2: x = (a * f) . xx by FUNCT_1:def 5;
reconsider xx = xx as Element of NAT by A1;
(a * f) . xx = a * (f . xx) by RVSUM_1:66;
hence x in NAT by A2; :: thesis: verum

end;

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