theorem :: DOMAIN_1:16

for d being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( d = x `4_4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 ) by MCART_1:78;