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

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum } c= 5 -tuples_on D

let x be object ; :: thesis: ( x in 5 -tuples_on D implies x in { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum } )
assume x in 5 -tuples_on D ; :: thesis: x in { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum }
then consider s being Element of D * such that
A1: x = s and
A2: len s = 5 ;
( 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5 ) ;
then ( 1 in dom s & 2 in dom s & 3 in dom s & 4 in dom s & 5 in dom s ) by A2, FINSEQ_1:def 3;
then reconsider d19 = s . 1, d29 = s . 2, d39 = s . 3, d49 = s . 4, d59 = s . 5 as Element of D by FINSEQ_2:11;
s = <*d19,d29,d39,d49,d59*> by A2, FINSEQ_4:78;
hence x in { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum } by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum } or x in 5 -tuples_on D )
assume x in { <*d1,d2,d3,d4,d5*> where d1, d2, d3, d4, d5 is Element of D : verum } ; :: thesis: x in 5 -tuples_on D
then consider d1, d2, d3, d4, d5 being Element of D such that
A3: x = <*d1,d2,d3,d4,d5*> ;
A4: len <*d1,d2,d3,d4,d5*> = 5 by FINSEQ_4:78;
<*d1,d2,d3,d4,d5*> is Element of D * by FINSEQ_1:def 11;
hence x in 5 -tuples_on D by A3, A4; :: thesis: verum