:: deftheorem defines |. QUATERNI:def 22 :
for z being Quaternion holds |.z.| = sqrt (((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2));