let A, a, b, c be set ; :: thesis: ( <*a,b,c*> in 3 -tuples_on A implies ( a in A & b in A & c in A ) )
A1: <*a,b,c*> . 3 = c by FINSEQ_1:62;
assume <*a,b,c*> in 3 -tuples_on A ; :: thesis: ( a in A & b in A & c in A )
then A2: ex a', b', c' being set st
( a' in A & b' in A & c' in A & <*a,b,c*> = <*a',b',c'*> ) by Th12;
( <*a,b,c*> . 1 = a & <*a,b,c*> . 2 = b ) by FINSEQ_1:62;
hence ( a in A & b in A & c in A ) by A2, A1, FINSEQ_1:62; :: thesis: verum