consider xx1 being Element of X1, xx2 being Element of X2, xx3 being Element of X3, xx4 being Element of X4 such that
A14:
x = [xx1,xx2,xx3,xx4]
by A1, Lm3;
take
xx4
; for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
xx4 = x4
thus
for x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] holds
xx4 = x4
by A14, Th33; verum