let X1, X2, X3, X4 be non empty set ; :: thesis: [:X1,X2,X3,X4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum }
defpred S₁[ set , set , set , set ] means verum;
A1: for x being Element of [:X1,X2,X3,X4:] holds x in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum }

proof

let x be Element of [:X1,X2,X3,X4:]; :: thesis: x in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum }
x = [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] ;
hence x in { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } ; :: thesis: verum

end;

for X1, X2, X3, X4 being non empty set holds { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : S₁[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:] from DOMAIN_1:sch 4();
then { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } is Subset of [:X1,X2,X3,X4:] ;
hence [:X1,X2,X3,X4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum } by A1, SUBSET_1:28; :: thesis: verum