now

let y be set ; :: thesis: ( y in rng (Seq fss) implies y in D )
assume y in rng (Seq fss) ; :: thesis: y in D
then consider x being set such that
A1: ( x in dom (Seq fss) & (Seq fss) . x = y ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A1;
consider n being Element of NAT such that
A2: ( n in dom fs & x <= n & y = fs . n ) by A1, GLIB_001:4;
y in rng fs by A2, FUNCT_1:def 5;
hence y in D ; :: thesis: verum

end;

then rng (Seq fss) c= D by TARSKI:def 3;
hence Seq fss is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum