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