let y, z be Element of X2; :: thesis: ( ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 ) & ( for x1, x2, x3 being set st x = [x1,x2,x3] holds
z = x2 ) implies y = z )
assume A7: for x1, x2, x3 being set st x = [x1,x2,x3] holds
y = x2 ; :: thesis: ( ex x1, x2, x3 being set st
( x = [x1,x2,x3] & not z = x2 ) or y = z )
assume A8: for x1, x2, x3 being set st x = [x1,x2,x3] holds
z = x2 ; :: thesis: y = z
consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A9: x = [xx1,xx2,xx3] by A1, Lm2;
y = xx2 by A9, A7;
hence y = z by A9, A8; :: thesis: verum