:: deftheorem defines `1_4 MCART_1:def 8 :
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
for b<sub>6</sub> being Element of X1 holds
( b<sub>6</sub> = x `1_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
b₆ = x1 );