let z1, z2 be quaternion number ; :: thesis: z1 - z2 = - (z2 - z1)
A1: Rea (z2 - z1) = (Rea z2) - (Rea z1) by Lm36;
A2: Im1 (z2 - z1) = (Im1 z2) - (Im1 z1) by Lm36;
A3: Im2 (z2 - z1) = (Im2 z2) - (Im2 z1) by Lm36;
Im3 (z2 - z1) = (Im3 z2) - (Im3 z1) by Lm36;
hence z1 - z2 = - (z2 - z1) by A1, A2, A3; :: thesis: verum