let D be non empty set ; :: thesis: 2 -tuples_on D = { <*d1,d2*> where d1, d2 is Element of D : verum }

now

let x be set ; :: thesis: ( ( x in 2 -tuples_on D implies x in { <*d1,d2*> where d1, d2 is Element of D : verum } ) & ( x in { <*d1,d2*> where d1, d2 is Element of D : verum } implies x in 2 -tuples_on D ) )
thus ( x in 2 -tuples_on D implies x in { <*d1,d2*> where d1, d2 is Element of D : verum } ) :: thesis: ( x in { <*d1,d2*> where d1, d2 is Element of D : verum } implies x in 2 -tuples_on D )

proof

assume x in 2 -tuples_on D ; :: thesis: x in { <*d1,d2*> where d1, d2 is Element of D : verum }
then consider s being Element of D * such that
A1: x = s and
A2: len s = 2 ;
( 1 in Seg 2 & 2 in Seg 2 ) ;
then ( 1 in dom s & 2 in dom s ) by A2, FINSEQ_1:def 3;
then reconsider d1' = s . 1, d2' = s . 2 as Element of D by Th13;
s = <*d1',d2'*> by A2, FINSEQ_1:61;
hence x in { <*d1,d2*> where d1, d2 is Element of D : verum } by A1; :: thesis: verum

end;

assume x in { <*d1,d2*> where d1, d2 is Element of D : verum } ; :: thesis: x in 2 -tuples_on D
then consider d1, d2 being Element of D such that
A3: x = <*d1,d2*> ;
<*d1,d2*> is FinSequence of D by Th15;
then ( len <*d1,d2*> = 2 & <*d1,d2*> is Element of D * ) by FINSEQ_1:61, FINSEQ_1:def 11;
hence x in 2 -tuples_on D by A3; :: thesis: verum

end;

hence 2 -tuples_on D = { <*d1,d2*> where d1, d2 is Element of D : verum } by TARSKI:2; :: thesis: verum