let A, a, b be set ; :: thesis: ( <*a,b*> in 2 -tuples_on A implies ( a in A & b in A ) )
assume <*a,b*> in 2 -tuples_on A ; :: thesis: ( a in A & b in A )
then consider a', b' being set such that
A1: ( a' in A & b' in A & <*a,b*> = <*a',b'*> ) by Th10;
( <*a,b*> . 1 = a & <*a,b*> . 2 = b & <*a',b'*> . 1 = a' & <*a',b'*> . 2 = b' ) by FINSEQ_1:61;
hence ( a in A & b in A ) by A1; :: thesis: verum