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