theorem :: DOMAIN_1:24

for X1, X2, X3 being non empty set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3 holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }