theorem :: QUATERNI:58

for z being Quaternion st Im1 z = 0 & Im2 z = 0 & Im3 z = 0 holds
z *' = z