let z1, z2 be quaternion number ; z1 - z2 = - (z2 - z1)
A1:
Rea (z2 - z1) = (Rea z2) - (Rea z1)
by Th42;
A2:
Im1 (z2 - z1) = (Im1 z2) - (Im1 z1)
by Th42;
A3:
Im2 (z2 - z1) = (Im2 z2) - (Im2 z1)
by Th42;
AA:
Im3 (z2 - z1) = (Im3 z2) - (Im3 z1)
by Th42;
B1:
Rea (- (z2 - z1)) = - ((Rea z2) - (Rea z1))
by A1, Th41;
B2:
Im1 (- (z2 - z1)) = - ((Im1 z2) - (Im1 z1))
by A2, Th41;
B3:
Im2 (- (z2 - z1)) = - ((Im2 z2) - (Im2 z1))
by A3, Th41;
BA:
Im3 (- (z2 - z1)) = - ((Im3 z2) - (Im3 z1))
by AA, Th41;
C2:
Rea (z1 - z2) = (Rea z1) - (Rea z2)
by Th42;
C3:
Im1 (z1 - z2) = (Im1 z1) - (Im1 z2)
by Th42;
C4:
Im2 (z1 - z2) = (Im2 z1) - (Im2 z2)
by Th42;
Im3 (z1 - z2) = (Im3 z1) - (Im3 z2)
by Th42;
hence
z1 - z2 = - (z2 - z1)
by Th25, C2, C3, C4, B1, B2, B3, BA; verum