let z1, z2 be quaternion number ; |.(z1 * z2).| ^2 = (|.z1.| ^2 ) * (|.z2.| ^2 )
set z3 = z1 * z2;
A1:
z1 * z2 = [*(((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))),(((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))),(((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))),(((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))*]
by QUATERN2:1;
A2:
( Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2)) & Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) )
by A1, QUATERNI:23;
A3:
( Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)) & Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)) )
by A1, QUATERNI:23;
A4:
( |.z1.| ^2 = ((((Rea z1) ^2 ) + ((Im1 z1) ^2 )) + ((Im2 z1) ^2 )) + ((Im3 z1) ^2 ) & |.z2.| ^2 = ((((Rea z2) ^2 ) + ((Im1 z2) ^2 )) + ((Im2 z2) ^2 )) + ((Im3 z2) ^2 ) )
by Th11;
thus
|.(z1 * z2).| ^2 = (|.z1.| ^2 ) * (|.z2.| ^2 )
by A4, A2, A3, Th11; verum