let c1, c2 be Quaternion; :: thesis: ( z + c1 = 0 & z + c2 = 0 implies c1 = c2 )
assume that
A5: z + c1 = 0 and
A6: z + c2 = 0 ; :: thesis: c1 = c2
consider x1, x2, x3, x4, y1, y2, y3, y4 being Real such that
A7: z = [*x1,x2,x3,x4*] and
A8: c1 = [*y1,y2,y3,y4*] and
A9: 0 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] by A5, Def6;
consider x19, x29, x39, x49, y19, y29, y39, y49 being Real such that
A10: z = [*x19,x29,x39,x49*] and
A11: c2 = [*y19,y29,y39,y49*] and
A12: 0 = [*(x19 + y19),(x29 + y29),(x39 + y39),(x49 + y49)*] by A6, Def6;
A13: x1 = x19 by A7, A10, Th5;
A14: x2 = x29 by A7, A10, Th5;
A15: x3 = x39 by A7, A10, Th5;
A16: x4 = x49 by A7, A10, Th5;
A17: x1 + y1 = 0 by A9, Lm6, Th5;
A18: x1 + y19 = 0 by A12, A13, Lm6, Th5;
A19: x2 + y2 = 0 by A9, Lm6, Th5;
A20: x2 + y29 = 0 by A12, A14, Lm6, Th5;
A21: x3 + y3 = 0 by A9, Lm6, Th5;
A22: x3 + y39 = 0 by A12, A15, Lm6, Th5;
A23: x4 + y4 = 0 by A9, Lm6, Th5;
x4 + y49 = 0 by A12, A16, Lm6, Th5;
hence c1 = c2 by A8, A11, A17, A18, A19, A20, A21, A22, A23; :: thesis: verum