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 set ; :: according to FINSEQ_1:def 19 :: thesis: ( x in X implies x is FinSequence )
assume x in X ; :: thesis: x is FinSequence
then x = the FinSequence by TARSKI:def 1;
hence x is FinSequence ; :: thesis: verum