theorem :: DOMAIN_1:25

for X1, X2, X3, X4 being non empty set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4 holds [:A1,A2,A3,A4:] = { [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 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }