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