let z1, z2 be Quaternion; :: thesis: |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2)
set z3 = z1 * z2;
A1: ( 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 QUATERNI:97;
A2: ( 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 QUATERNI:97;
( |.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;
hence |.(z1 * z2).| ^2 = (|.z1.| ^2) * (|.z2.| ^2) by A1, A2, Th11; :: thesis: verum