consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A10: x = [xx1,xx2,xx3] by A1, Lm2;
take xx3 ; :: thesis: for x1, x2, x3 being set st x = [x1,x2,x3] holds
xx3 = x3
thus for x1, x2, x3 being set st x = [x1,x2,x3] holds
xx3 = x3 by A10, Th28; :: thesis: verum