theorem :: QUATERNI:61

for z being Quaternion holds
( Rea (z + (z *')) = 2 * (Rea z) & Im1 (z + (z *')) = 0 & Im2 (z + (z *')) = 0 & Im3 (z + (z *')) = 0 )