let z1, z be Quaternion; ( z is Real implies (z * z1) *' = (z *') * (z1 *') )
A1:
( Im1 (z1 *') = - (Im1 z1) & Im2 (z1 *') = - (Im2 z1) )
by QUATERNI:44;
A2:
( Im3 (z1 *') = - (Im3 z1) & Rea (z *') = Rea z )
by QUATERNI:44;
A3:
Rea (z * z1) = ((((Rea z) * (Rea z1)) - ((Im1 z) * (Im1 z1))) - ((Im2 z) * (Im2 z1))) - ((Im3 z) * (Im3 z1))
by QUATERNI:97;
assume A4:
z is Real
; (z * z1) *' = (z *') * (z1 *')
then reconsider x = z as Real ;
A5:
( Im1 z = 0 & Im2 z = 0 )
by A4, Lm1;
A6:
Im3 z = 0
by A4, Lm1;
A7:
Im3 (z *') = - (Im3 z)
by QUATERNI:44;
A8:
( Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) )
by QUATERNI:44;
A9:
Im3 (z * z1) = ((((Rea z) * (Im3 z1)) + ((Im3 z) * (Rea z1))) + ((Im1 z) * (Im2 z1))) - ((Im2 z) * (Im1 z1))
by QUATERNI:97;
A10:
Im2 (z * z1) = ((((Rea z) * (Im2 z1)) + ((Im2 z) * (Rea z1))) + ((Im3 z) * (Im1 z1))) - ((Im1 z) * (Im3 z1))
by QUATERNI:97;
A11:
Im1 (z * z1) = ((((Rea z) * (Im1 z1)) + ((Im1 z) * (Rea z1))) + ((Im2 z) * (Im3 z1))) - ((Im3 z) * (Im2 z1))
by QUATERNI:97;
set z3 = z *' ;
set z2 = z1 *' ;
A12:
(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 *')))) * <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 QUATERNI:93;
(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 A3, 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 A11, 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 A10, 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 A9, QUATERNI:44
;
hence
(z * z1) *' = (z *') * (z1 *')
by A5, A6, A1, A2, A8, A7, A12, QUATERNI:44; verum