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