let c1, c2 be quaternion number ; :: thesis: ( z + c1 = 0 & z + c2 = 0 implies c1 = c2 )
assume that
A2: z + c1 = 0 and
A3: z + c2 = 0 ; :: thesis: c1 = c2
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of REAL such that
A4: z = [*x1,x2,x3,x4*] and
A5: c1 = [*y1,y2,y3,y4*] and
A6: 0 = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] by A2, Def7;
consider x1', x2', x3', x4', y1', y2', y3', y4' being Element of REAL such that
A7: z = [*x1',x2',x3',x4'*] and
A8: c2 = [*y1',y2',y3',y4'*] and
A9: 0 = [*(x1' + y1'),(x2' + y2'),(x3' + y3'),(x4' + y4')*] by A3, Def7;
A10: ( x1 = x1' & x2 = x2' & x3 = x3' & x4 = x4' ) by A4, A7, Th12;
A11: x1 + y1 = 0 by A6, Lm5, Th12;
A12: x1 + y1' = 0 by A9, A10, Lm5, Th12;
A13: x2 + y2 = 0 by A6, Lm5, Th12;
A14: x2 + y2' = 0 by A9, A10, Lm5, Th12;
A15: x3 + y3 = 0 by A6, Lm5, Th12;
A16: x3 + y3' = 0 by A9, A10, Lm5, Th12;
A17: x4 + y4 = 0 by A6, Lm5, Th12;
x4 + y4' = 0 by A9, A10, Lm5, Th12;
hence c1 = c2 by A5, A8, A11, A12, A13, A14, A15, A16, A17; :: thesis: verum