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 a9, b9, c9 being set st
( a9 in A & b9 in A & c9 in A & <*a,b,c*> = <*a9,b9,c9*> ) 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