let z be Quaternion; :: thesis: |.z.| ^2 = Rea (z * (z *'))
Rea (z * (z *')) = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) by QUATERNI:60;
hence |.z.| ^2 = Rea (z * (z *')) by Th11; :: thesis: verum