theorem :: QUATERN3:3

for z3, z being quaternion number st z is Real holds
z - z3 = [*((Rea z) - (Rea z3)),(- (Im1 z3)),(- (Im2 z3)),(- (Im3 z3))*]