take [*(x + y1),y2,y3,y4*] ; :: thesis: ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & [*(x + y1),y2,y3,y4*] = [*(x + y1),y2,y3,y4*] )
thus ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & [*(x + y1),y2,y3,y4*] = [*(x + y1),y2,y3,y4*] ) by A1; :: thesis: verum