let X be set ; :: thesis: for x being object st <*x*> is FinSequence of X holds
x in X
let x be object ; :: thesis: ( <*x*> is FinSequence of X implies x in X )
A1: rng <*x*> = {x} by FINSEQ_1:38;
assume <*x*> is FinSequence of X ; :: thesis: x in X
then {x} c= X by A1, FINSEQ_1:def 4;
hence x in X by ZFMISC_1:31; :: thesis: verum