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

now :: thesis: for x being object holds
( ( 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 ) )

let x be object ; :: 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 ;
2 in Seg 2 ;
then A3: 2 in dom s by A2, FINSEQ_1:def 3;
1 in Seg 2 ;
then 1 in dom s by A2, FINSEQ_1:def 3;
then reconsider d19 = s . 1, d29 = s . 2 as Element of D by A3, Th9;
s = <*d19,d29*> by A2, FINSEQ_1:44;
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
A4: x = <*d1,d2*> ;
<*d1,d2*> is FinSequence of D by Th11;
then ( len <*d1,d2*> = 2 & <*d1,d2*> is Element of D * ) by FINSEQ_1:44, FINSEQ_1:def 11;
hence x in 2 -tuples_on D by A4; :: thesis: verum

end;

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