theorem :: DOMAIN_1:8

for c being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( c = x `3_3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 ) by MCART_1:67;