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