A1: [:(rng f1),(rng f2):] c= [:D,D:] by ZFMISC_1:96;
rng <:f1,f2:> c= [:(rng f1),(rng f2):] by FUNCT_3:51;
then rng <:f1,f2:> c= [:D,D:] by A1;
hence <:f1,f2:> is FinSequence of [:D,D:] by FINSEQ_1:def 4; :: thesis: verum