let z1, z2 be Quaternion; :: thesis: Rea (z1 * z2) = Rea (z2 * z1)
Rea (z2 * z1) = ((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1)) by QUATERNI:97;
hence Rea (z1 * z2) = Rea (z2 * z1) by QUATERNI:97; :: thesis: verum