let X be set ; :: thesis: ( X is empty implies X is FinSequence-membered )
assume A1: X is empty ; :: thesis: X is FinSequence-membered
let x be set ; :: according to FINSEQ_1:def 18 :: thesis: ( x in X implies x is FinSequence )
assume x in X ; :: thesis: x is FinSequence
hence x is FinSequence by A1; :: thesis: verum