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