theorem Th11: :: QUATERN3:11
for z being quaternion number holds |.z.| ^2 = ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2)