let z1, z be Quaternion; :: thesis: ( z is Real implies z * z1 = z1 * z )
assume A1: z is Real ; :: thesis: z * z1 = z1 * z
then A2: Im3 z = 0 by Lm1;
A3: ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm1;
z1 * z = (((((((Rea z1) * (Rea z)) - ((Im1 z1) * (Im1 z))) - ((Im2 z1) * (Im2 z))) - ((Im3 z1) * (Im3 z))) + ((((((Rea z1) * (Im1 z)) + ((Im1 z1) * (Rea z))) + ((Im2 z1) * (Im3 z))) - ((Im3 z1) * (Im2 z))) * <i>)) + ((((((Rea z1) * (Im2 z)) + ((Im2 z1) * (Rea z))) + ((Im3 z1) * (Im1 z))) - ((Im1 z1) * (Im3 z))) * <j>)) + ((((((Rea z1) * (Im3 z)) + ((Im3 z1) * (Rea z))) + ((Im1 z1) * (Im2 z))) - ((Im2 z1) * (Im1 z))) * <k>) by QUATERNI:93;
hence z * z1 = z1 * z by A2, A3, QUATERNI:93; :: thesis: verum