rng (Seq (f | A)) c= NAT by RELAT_1:def 19;
hence Seq (f | A) is FinSequence of NAT by FINSEQ_1:def 4; :: thesis: verum