let c1, c2 be Number ; :: thesis: ( ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & c1 = [*(x + y1),y2,y3,y4*] ) & ex y1, y2, y3, y4 being Real st
( y = [*y1,y2,y3,y4*] & c2 = [*(x + y1),y2,y3,y4*] ) implies c1 = c2 )
given y1, y2, y3, y4 being Real such that A2: y = [*y1,y2,y3,y4*] and
A3: c1 = [*(x + y1),y2,y3,y4*] ; :: thesis: ( for y1, y2, y3, y4 being Real holds
( not y = [*y1,y2,y3,y4*] or not c2 = [*(x + y1),y2,y3,y4*] ) or c1 = c2 )
given y19, y29, y39, y49 being Real such that A4: y = [*y19,y29,y39,y49*] and
A5: c2 = [*(x + y19),y29,y39,y49*] ; :: thesis: c1 = c2
A6: y1 = y19 by A2, A4, Th5;
A7: y2 = y29 by A2, A4, Th5;
y3 = y39 by A2, A4, Th5;
hence c1 = c2 by A2, A3, A4, A5, A6, A7, Th5; :: thesis: verum