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

now :: thesis: for x being object holds
( ( x in 3 -tuples_on D implies x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } ) & ( x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } implies x in 3 -tuples_on D ) )

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

proof

assume x in 3 -tuples_on D ; :: thesis: x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }
then consider s being Element of D * such that
A1: x = s and
A2: len s = 3 ;
2 in Seg 3 ;
then A3: 2 in dom s by A2, FINSEQ_1:def 3;
3 in Seg 3 ;
then A4: 3 in dom s by A2, FINSEQ_1:def 3;
1 in Seg 3 ;
then 1 in dom s by A2, FINSEQ_1:def 3;
then reconsider d19 = s . 1, d29 = s . 2, d39 = s . 3 as Element of D by A3, A4, Th9;
s = <*d19,d29,d39*> by A2, FINSEQ_1:45;
hence x in { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum } by A1; :: thesis: verum

end;

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

end;

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