take y5 ; :: thesis: for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
y5 = y5
thus for y1, y2, y3, y4, y5 being object st x = [y1,y2,y3,y4,y5] holds
y5 = y5 by A1, Th10; :: thesis: verum