now :: thesis: for a being object st a in { s where s is Element of D * : len s = i } holds
a is FinSequence of D

let a be object ; :: thesis: ( a in { s where s is Element of D * : len s = i } implies a is FinSequence of D )
assume a in { s where s is Element of D * : len s = i } ; :: thesis: a is FinSequence of D
then ex s being Element of D * st
( s = a & len s = i ) ;
hence a is FinSequence of D ; :: thesis: verum

end;

hence { s where s is Element of D * : len s = i } is FinSequenceSet of D by Def3; :: thesis: verum