theorem :: QUATERNI:44

for z being Quaternion holds
( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) )