let A be set ; :: thesis: for a being object st <*a*> in 1 -tuples_on A holds
a in A
let a be object ; :: thesis: ( <*a*> in 1 -tuples_on A implies a in A )
assume <*a*> in 1 -tuples_on A ; :: thesis: a in A
then A1: ex a9 being set st
( a9 in A & <*a*> = <*a9*> ) by Th133;
<*a*> . 1 = a by FINSEQ_1:40;
hence a in A by A1, FINSEQ_1:40; :: thesis: verum