let c1, c2 be Number ; :: thesis: ( ex x1, x2, x3, x4, y1, y2, y3, y4 being 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 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 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 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 x19, x29, x39, x49, y19, y29, y39, y49 being Real such that A6: x = [*x19,x29,x39,x49*] and
A7: y = [*y19,y29,y39,y49*] and
A8: c2 = [*(x19 + y19),(x29 + y29),(x39 + y39),(x49 + y49)*] ; :: thesis: c1 = c2
A9: x1 = x19 by A3, A6, Th5;
A10: x2 = x29 by A3, A6, Th5;
A11: x3 = x39 by A3, A6, Th5;
A12: x4 = x49 by A3, A6, Th5;
A13: y1 = y19 by A4, A7, Th5;
A14: y2 = y29 by A4, A7, Th5;
y3 = y39 by A4, A7, Th5;
hence c1 = c2 by A4, A5, A7, A8, A9, A10, A11, A12, A13, A14, Th5; :: thesis: verum