take x2 ; :: thesis: for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
x2 = y2
thus for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
x2 = y2 by A1, MCART_1:29; :: thesis: verum