theorem Th32: :: QUATERN3:32

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