let z, z1 be quaternion number ; :: thesis: ( z is Real implies z * z1 = z1 * z )
assume z is Real ; :: thesis: z * z1 = z1 * z
then reconsider x = z as Real ;
( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )

proof

B2: x = [*x,0 *] by ARYTM_0:def 7;
[*x,0 *] = [*x,0 ,0 ,0 *] by QUATERNI:def 6;
hence ( Rea z = x & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by B2, QUATERNI:23; :: thesis: verum

end;

hence z * z1 = z1 * z ; :: thesis: verum