let c1, c2 be quaternion number ; :: 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 Element of 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, Def7;
consider x1', x2', x3', x4', y1', y2', y3', y4' being Element of REAL such that
A10: z = [*x1',x2',x3',x4'*] and
A11: c2 = [*y1',y2',y3',y4'*] and
A12: 0 = [*(x1' + y1'),(x2' + y2'),(x3' + y3'),(x4' + y4')*] by A6, Def7;
A13: x1 = x1' by A7, A10, Th12;
A14: x2 = x2' by A7, A10, Th12;
A15: x3 = x3' by A7, A10, Th12;
A16: x4 = x4' by A7, A10, Th12;
A17: x1 + y1 = 0 by A9, Lm7, Th12;
A18: x1 + y1' = 0 by A12, A13, Lm7, Th12;
A19: x2 + y2 = 0 by A9, Lm7, Th12;
A20: x2 + y2' = 0 by A12, A14, Lm7, Th12;
A21: x3 + y3 = 0 by A9, Lm7, Th12;
A22: x3 + y3' = 0 by A12, A15, Lm7, Th12;
A23: x4 + y4 = 0 by A9, Lm7, Th12;
x4 + y4' = 0 by A12, A16, Lm7, Th12;
hence c1 = c2 by A8, A11, A17, A18, A19, A20, A21, A22, A23; :: thesis: verum