let y be Element of X1; ( y = x `1_4 iff for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
y = x1 )
thus
( y = x `1_4 implies for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
y = x1 )
; ( ( for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
y = x1 ) implies y = x `1_4 )
assume A2:
for x1, x2, x3, x4 being object st x = [x1,x2,x3,x4] holds
y = x1
; y = x `1_4
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A3:
x = [xx1,xx2,xx3,xx4]
by Lm3;
thus
y = x `1_4
by A2, A3; verum