consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A10: x = [xx1,xx2,xx3,xx4] by Lm3;
thus x `4_4 is Element of X4 by A10; :: thesis: verum