let c1, c2 be number ; :: thesis: ( ex y1, y2, y3, y4 being Element of REAL st
( y = [*y1,y2,y3,y4*] & c1 = [*(x + y1),y2,y3,y4*] ) & ex y1, y2, y3, y4 being Element of 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 Element of REAL holds
( not y = [*y1,y2,y3,y4*] or not c2 = [*(x + y1),y2,y3,y4*] ) or c1 = c2 )
given y1', y2', y3', y4' being Real such that A4: y = [*y1',y2',y3',y4'*] and
A5: c2 = [*(x + y1'),y2',y3',y4'*] ; :: thesis: c1 = c2
A6: y1 = y1' by A2, A4, Th12;
A7: y2 = y2' by A2, A4, Th12;
y3 = y3' by A2, A4, Th12;
hence c1 = c2 by A2, A3, A4, A5, A6, A7, Th12; :: thesis: verum