theorem :: MCART_1:64

for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:]
for x1, x2, x3 being object st x = [x1,x2,x3] holds
( x `1_3 = x1 & x `2_3 = x2 & x `3_3 = x3 ) ;