let z1, z2 be quaternion number ; :: thesis: Rea (z1 * z2) = Rea (z2 * z1)
z2 * z1 = [*(((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1))),(((((Rea z2) * (Im1 z1)) + ((Im1 z2) * (Rea z1))) + ((Im2 z2) * (Im3 z1))) - ((Im3 z2) * (Im2 z1))),(((((Rea z2) * (Im2 z1)) + ((Im2 z2) * (Rea z1))) + ((Im3 z2) * (Im1 z1))) - ((Im1 z2) * (Im3 z1))),(((((Rea z2) * (Im3 z1)) + ((Im3 z2) * (Rea z1))) + ((Im1 z2) * (Im2 z1))) - ((Im2 z2) * (Im1 z1)))*] by QUATERN2:1;
then ( 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)))*] & Rea (z2 * z1) = ((((Rea z2) * (Rea z1)) - ((Im1 z2) * (Im1 z1))) - ((Im2 z2) * (Im2 z1))) - ((Im3 z2) * (Im3 z1)) ) by QUATERN2:1, QUATERNI:23;
hence Rea (z1 * z2) = Rea (z2 * z1) by QUATERNI:23; :: thesis: verum