let z1, z2 be quaternion number ; :: thesis: |.(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)) & Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)) & 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 Lm16;
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));
A2: ( ((((((((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 ) >= 0 & ((((Rea z1) ^2 ) + ((Im1 z1) ^2 )) + ((Im2 z1) ^2 )) + ((Im3 z1) ^2 ) >= 0 & ((((Rea z2) ^2 ) + ((Im1 z2) ^2 )) + ((Im2 z2) ^2 )) + ((Im3 z2) ^2 ) >= 0 ) by Lm21;
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, SQUARE_1:97; :: thesis: verum