let z1, z2 be quaternion number ; :: thesis: (z1 * z2) ~ = (z1 ~ ) * (z2 ~ )
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;
then ( 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 QUATERNI:23;
hence (z1 * z2) ~ = (z1 ~ ) * (z2 ~ ) ; :: thesis: verum