let z1, z2 be Quaternion; z1 - z2 = - (z2 - z1)
A1:
Rea (z2 - z1) = (Rea z2) - (Rea z1)
by Th35;
A2:
Im1 (z2 - z1) = (Im1 z2) - (Im1 z1)
by Th35;
A3:
Im2 (z2 - z1) = (Im2 z2) - (Im2 z1)
by Th35;
A4:
Im3 (z2 - z1) = (Im3 z2) - (Im3 z1)
by Th35;
A5:
Rea (- (z2 - z1)) = - ((Rea z2) - (Rea z1))
by A1, Th34;
A6:
Im1 (- (z2 - z1)) = - ((Im1 z2) - (Im1 z1))
by A2, Th34;
A7:
Im2 (- (z2 - z1)) = - ((Im2 z2) - (Im2 z1))
by A3, Th34;
A8:
Im3 (- (z2 - z1)) = - ((Im3 z2) - (Im3 z1))
by A4, Th34;
A9:
Rea (z1 - z2) = (Rea z1) - (Rea z2)
by Th35;
A10:
Im1 (z1 - z2) = (Im1 z1) - (Im1 z2)
by Th35;
A11:
Im2 (z1 - z2) = (Im2 z1) - (Im2 z2)
by Th35;
Im3 (z1 - z2) = (Im3 z1) - (Im3 z2)
by Th35;
hence
z1 - z2 = - (z2 - z1)
by Th18, A9, A10, A11, A5, A6, A7, A8; verum