let x be set ; :: according to FINSEQ_1:def 19 :: thesis: ( x in X * implies x is FinSequence )
assume x in X * ; :: thesis: x is FinSequence
hence x is FinSequence by Def11; :: thesis: verum