take X = { the FinSequence}; :: thesis: ( not X is empty & X is FinSequence-membered )
thus not X is empty ; :: thesis: X is FinSequence-membered
let x be object ; :: according to FINSEQ_1:def 18 :: thesis: ( x in X implies x is FinSequence )
thus ( x in X implies x is FinSequence ) by TARSKI:def 1; :: thesis: verum