let z1, z2 be Quaternion; z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*]
A1:
z1 = [*(Rea z1),(Im1 z1),(Im2 z1),(Im3 z1)*]
by Th17;
A2:
z2 = [*(Rea z2),(Im1 z2),(Im2 z2),(Im3 z2)*]
by Th17;
set z9 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*];
z2 + [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] =
[*((Rea z2) + (- (Rea z2))),((Im1 z2) + (- (Im1 z2))),((Im2 z2) + (- (Im2 z2))),((Im3 z2) + (- (Im3 z2)))*]
by A2, Def6
.=
0
by Lm6
;
then
- z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*]
by Def7;
hence
z1 - z2 = [*((Rea z1) - (Rea z2)),((Im1 z1) - (Im1 z2)),((Im2 z1) - (Im2 z2)),((Im3 z1) - (Im3 z2))*]
by A1, Def6; verum