theorem :: QUATERN3:13

for z being Quaternion holds |.z.| ^2 = Rea (z * (z *'))