let A be set ; :: thesis: for a, b, c being object st <*a,b,c*> in 3 -tuples_on A holds
( a in A & b in A & c in A )
let a, b, c be object ; :: 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 ;
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 object st
( a9 in A & b9 in A & c9 in A & <*a,b,c*> = <*a9,b9,c9*> ) by Th137;
( <*a,b,c*> . 1 = a & <*a,b,c*> . 2 = b ) ;
hence ( a in A & b in A & c in A ) by A2, A1, FINSEQ_1:45; :: thesis: verum