let x, X be set ; :: thesis: ( <*x*> is FinSequence of X implies x in X )
assume A1: <*x*> is FinSequence of X ; :: thesis: x in X
rng <*x*> = {x} by FINSEQ_1:55;
then {x} c= X by A1, FINSEQ_1:def 4;
hence x in X by ZFMISC_1:37; :: thesis: verum