A1: f * T is FinSequence of NAT by FINSEQ_2:32;
rng (f * T) c= REAL ;
hence T (#) f is FinSequence of REAL by A1, FINSEQ_1:def 4; :: thesis: verum