theorem :: DOMAIN_1:21

for X1, X2, X3, X4 being non empty set holds [: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 }