let y be Element of X2; :: thesis: ( y = x `2_3 iff for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 )
thus ( y = x `2_3 implies for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 ) :: thesis: ( ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 ) implies y = x `2_3 )

proof

assume Z: y = x `2_3 ; :: thesis: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2
let x1, x2, x3 be set ; :: thesis: ( x = [x1,x2,x3] implies y = x2 )
assume W: x = [x1,x2,x3] ; :: thesis: y = x2
[x1,x2,x3] `2_3 = x2 ;
hence y = x2 by W, Z; :: thesis: verum

end;

assume Z: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 ; :: thesis: y = x `2_3
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
[xx1,xx2,xx3] `2_3 = xx2 ;
hence y = x `2_3 by Z, A6; :: thesis: verum