let z, z1 be quaternion number ; :: thesis: ( z is Real implies z * z1 = z1 * z )
assume A1: z is Real ; :: thesis: z * z1 = z1 * z
A2: Im3 z = 0 by A1, Lm2;
reconsider x = z as Real by A1;
A3: ( Im1 z = 0 & Im2 z = 0 ) by A1, Lm2;
thus z * z1 = z1 * z by A3, A2; :: thesis: verum