let D be set ; :: thesis: D * is FinSequenceSet of D
D * is FinSequenceSet of D

proof

let a be object ; :: according to FINSEQ_2:def 3 :: thesis: ( a in D * implies a is FinSequence of D )
thus ( a in D * implies a is FinSequence of D ) by FINSEQ_1:def 11; :: thesis: verum

end;

hence D * is FinSequenceSet of D ; :: thesis: verum