consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3 such that
A7: x = [xx1,xx2,xx3] by Lm2;
thus x `3_3 is Element of X3 by A7; :: thesis: verum