theorem :: QUATERNI:88

for z being Quaternion holds |.(z * z).| = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)