let c1, c2 be number ; :: thesis: ( ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & c1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) & ex x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL st
( x = [*x1,x2,x3,x4*] & y = [*y1,y2,y3,y4*] & c2 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) implies c1 = c2 )
given x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL such that A3: x = [*x1,x2,x3,x4*] and
A4: y = [*y1,y2,y3,y4*] and
A5: c1 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ; :: thesis: ( for x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL holds
( not x = [*x1,x2,x3,x4*] or not y = [*y1,y2,y3,y4*] or not c2 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] ) or c1 = c2 )
given x1', x2', x3', x4', y1', y2', y3', y4' being Element of REAL such that A6: x = [*x1',x2',x3',x4'*] and
A7: y = [*y1',y2',y3',y4'*] and
A8: c2 = [*(x1' + y1'),(x2' + y2'),(x3' + y3'),(x4' + y4')*] ; :: thesis: c1 = c2
A9: x1 = x1' by A3, A6, Th12;
A10: x2 = x2' by A3, A6, Th12;
A11: x3 = x3' by A3, A6, Th12;
A12: x4 = x4' by A3, A6, Th12;
A13: y1 = y1' by A4, A7, Th12;
A14: y2 = y2' by A4, A7, Th12;
y3 = y3' by A4, A7, Th12;
hence c1 = c2 by A4, A5, A7, A8, A9, A10, A11, A12, A13, A14, Th12; :: thesis: verum