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