for y1 being object for X1, X2, X3, X4 being non emptyset for x being Element of [:X1,X2,X3,X4:] st ( for xx1 being Element of X1 for xx2 being Element of X2 for xx3 being Element of X3 for xx4 being Element of X4 st x =[xx1,xx2,xx3,xx4] holds y1 = xx1 ) holds y1 = x `1_4