let z, z1 be quaternion number ; :: thesis: ( z is Real implies (z * z1) *' = (z *' ) * (z1 *' ) )
assume z is Real ; :: thesis: (z * z1) *' = (z *' ) * (z1 *' )
then reconsider x = z as Real ;
B: ( 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;

z * z1 = [*(((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))),(((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1))),(((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1))),(((((Rea z) * (Im3 z1)) + ((Im3 z) * (Rea z1))) + ((Im1 z) * (Im2 z1))) - ((Im2 z) * (Im1 z1)))*] by QUATERN2:1;
then a: ( Rea (z * z1) = ((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1)) & Im1 (z * z1) = ((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)) & Im2 (z * z1) = ((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)) & Im3 (z * z1) = ((((Rea z) * (Im3 z1)) + ((Im3 z) * (Rea z1))) + ((Im1 z) * (Im2 z1))) - ((Im2 z) * (Im1 z1)) ) by QUATERNI:23;
B1: ( Rea (z1 *' ) = Rea z1 & Im1 (z1 *' ) = - (Im1 z1) & Im2 (z1 *' ) = - (Im2 z1) & Im3 (z1 *' ) = - (Im3 z1) ) by QUATERNI:44;
B2: ( Rea (z *' ) = Rea z & Im1 (z *' ) = - (Im1 z) & Im2 (z *' ) = - (Im2 z) & Im3 (z *' ) = - (Im3 z) ) by QUATERNI:44;
(z * z1) *' = (((Rea ((z * z1) *' )) + ((Im1 ((z * z1) *' )) * <i> )) + ((Im2 ((z * z1) *' )) * <j> )) + ((Im3 ((z * z1) *' )) * <k> ) by QUATERNI:37
.= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((Im1 ((z * z1) *' )) * <i> )) + ((Im2 ((z * z1) *' )) * <j> )) + ((Im3 ((z * z1) *' )) * <k> ) by a, QUATERNI:44
.= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * <i> )) + ((Im2 ((z * z1) *' )) * <j> )) + ((Im3 ((z * z1) *' )) * <k> ) by a, QUATERNI:44
.= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * <i> )) + ((- (((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)))) * <j> )) + ((Im3 ((z * z1) *' )) * <k> ) by a, QUATERNI:44
.= (((((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))) + ((- (((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1)))) * <i> )) + ((- (((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1)))) * <j> )) + ((- (((((Rea z) * (Im3 z1)) + ((Im3 z) * (Rea z1))) + ((Im1 z) * (Im2 z1))) - ((Im2 z) * (Im1 z1)))) * <k> ) by a, QUATERNI:44 ;
hence (z * z1) *' = (z *' ) * (z1 *' ) by B, B2, B1; :: thesis: verum