theorem :: QUATERN3:14

for z being Quaternion holds 2 * (Rea z) = Rea (z + (z *'))