let z1, z2 be Quaternion; z1 = (z1 + z2) - 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;
A3:
- z2 = [*(- (Rea z2)),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*]
by Th55;
z1 + z2 = [*((Rea z1) + (Rea z2)),((Im1 z1) + (Im1 z2)),((Im2 z1) + (Im2 z2)),((Im3 z1) + (Im3 z2))*]
by A1, A2, Def6;
then
(z1 + z2) - z2 = [*(((Rea z1) + (Rea z2)) - (Rea z2)),(((Im1 z1) + (Im1 z2)) - (Im1 z2)),(((Im2 z1) + (Im2 z2)) - (Im2 z2)),(((Im3 z1) + (Im3 z2)) - (Im3 z2))*]
by A3, Def6;
hence
z1 = (z1 + z2) - z2
by Th17; verum