now :: thesis: for y being object st y in rng (Seq fss) holds
y in D
let y be object ; :: thesis: ( y in rng (Seq fss) implies y in D )
assume y in rng (Seq fss) ; :: thesis: y in D
then consider x being object such that
A1: x in dom (Seq fss) and
A2: (Seq fss) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A1;
ex n being Element of NAT st
( n in dom fs & x <= n & y = fs . n ) by A1, A2, GLIB_001:4;
then y in rng fs by FUNCT_1:def 3;
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