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

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

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

end;

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