take D * ; :: thesis: for a being object st a in D * holds
a is FinSequence of D
thus for a being object st a in D * holds
a is FinSequence of D by FINSEQ_1:def 11; :: thesis: verum