take x4 ; :: thesis: for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
x4 = y4
thus for y1, y2, y3, y4, y5 being set st x = [y1,y2,y3,y4,y5] holds
x4 = y4 by A1, MCART_2:7; :: thesis: verum