let z1, z2 be Quaternion; |.(z1 * z2).| = |.z1.| * |.z2.|
set m1 = Rea z1;
set m2 = Im1 z1;
set m3 = Im2 z1;
set m4 = Im3 z1;
set n1 = Rea z2;
set n2 = Im1 z2;
set n3 = Im2 z2;
set n4 = Im3 z2;
A1:
Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))
by Lm17;
A2:
Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))
by Lm17;
A3:
Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))
by Lm17;
A4:
Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))
by Lm17;
set b1 = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2));
set b2 = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2));
set b3 = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2));
set b4 = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2));
A5:
((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2) >= 0
by Th67;
A6:
((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2) >= 0
by Th67;
sqrt (((((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) ^2) + ((((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))) ^2)) + ((((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))) ^2)) + ((((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))) ^2)) = sqrt ((((((Rea z1) ^2) + ((Im1 z1) ^2)) + ((Im2 z1) ^2)) + ((Im3 z1) ^2)) * (((((Rea z2) ^2) + ((Im1 z2) ^2)) + ((Im2 z2) ^2)) + ((Im3 z2) ^2)))
;
hence
|.(z1 * z2).| = |.z1.| * |.z2.|
by A1, A2, A3, A4, A5, A6, SQUARE_1:29; verum