let y be Element of X3; ( y = x `2 iff for x1, x2, x3 being object st x = [x1,x2,x3] holds
y = x3 )
thus
( y = x `3_3 implies for x1, x2, x3 being object st x = [x1,x2,x3] holds
y = x3 )
; ( ( for x1, x2, x3 being object st x = [x1,x2,x3] holds
y = x3 ) implies y = x `2 )
assume A8:
for x1, x2, x3 being object st x = [x1,x2,x3] holds
y = x3
; y = x `2
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A9:
x = [xx1,xx2,xx3]
by Lm2;
thus
y = x `3_3
by A8, A9; verum