A1: rng (Seq (f | A)) c= rng (f | A) by RELAT_1:45;
A2: rng f c= NAT by RELAT_1:def 19;
rng (f | A) c= rng f by RELAT_1:99;
then rng (f | A) c= NAT by A2, XBOOLE_1:1;
then rng (Seq (f | A)) c= NAT by A1, XBOOLE_1:1;
hence Seq (f | A) is FinSequence of NAT by FINSEQ_1:def 4; :: thesis: verum