theorem :: MCART_1:74

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