let z1, z2 be quaternion number ; (z1 * z2) *' = (z2 *') * (z1 *')
A1:
( Rea (z2 *') = Rea z2 & Im1 (z2 *') = - (Im1 z2) )
by QUATERNI:44;
A2:
( Im2 (z2 *') = - (Im2 z2) & Im3 (z2 *') = - (Im3 z2) )
by QUATERNI:44;
A3:
Rea (z1 * z2) = ((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))
by QUATERNI:97;
A4:
Im3 (z1 * z2) = ((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2))
by QUATERNI:97;
A5:
( Im2 (z1 *') = - (Im2 z1) & Im3 (z1 *') = - (Im3 z1) )
by QUATERNI:44;
A6:
( Rea (z1 *') = Rea z1 & Im1 (z1 *') = - (Im1 z1) )
by QUATERNI:44;
A7:
Im2 (z1 * z2) = ((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2))
by QUATERNI:97;
A8:
Im1 (z1 * z2) = ((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2))
by QUATERNI:97;
set z3 = z2 *' ;
set z4 = z1 *' ;
A9:
(z2 *') * (z1 *') = (((((((Rea (z2 *')) * (Rea (z1 *'))) - ((Im1 (z2 *')) * (Im1 (z1 *')))) - ((Im2 (z2 *')) * (Im2 (z1 *')))) - ((Im3 (z2 *')) * (Im3 (z1 *')))) + ((((((Rea (z2 *')) * (Im1 (z1 *'))) + ((Im1 (z2 *')) * (Rea (z1 *')))) + ((Im2 (z2 *')) * (Im3 (z1 *')))) - ((Im3 (z2 *')) * (Im2 (z1 *')))) * <i>)) + ((((((Rea (z2 *')) * (Im2 (z1 *'))) + ((Im2 (z2 *')) * (Rea (z1 *')))) + ((Im3 (z2 *')) * (Im1 (z1 *')))) - ((Im1 (z2 *')) * (Im3 (z1 *')))) * <j>)) + ((((((Rea (z2 *')) * (Im3 (z1 *'))) + ((Im3 (z2 *')) * (Rea (z1 *')))) + ((Im1 (z2 *')) * (Im2 (z1 *')))) - ((Im2 (z2 *')) * (Im1 (z1 *')))) * <k>)
by QUATERNI:93;
(z1 * z2) *' =
(((Rea ((z1 * z2) *')) + ((Im1 ((z1 * z2) *')) * <i>)) + ((Im2 ((z1 * z2) *')) * <j>)) + ((Im3 ((z1 * z2) *')) * <k>)
by QUATERNI:37
.=
(((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((Im1 ((z1 * z2) *')) * <i>)) + ((Im2 ((z1 * z2) *')) * <j>)) + ((Im3 ((z1 * z2) *')) * <k>)
by A3, QUATERNI:44
.=
(((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i>)) + ((Im2 ((z1 * z2) *')) * <j>)) + ((Im3 ((z1 * z2) *')) * <k>)
by A8, QUATERNI:44
.=
(((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i>)) + ((- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))) * <j>)) + ((Im3 ((z1 * z2) *')) * <k>)
by A7, QUATERNI:44
.=
(((((((Rea z1) * (Rea z2)) - ((Im1 z1) * (Im1 z2))) - ((Im2 z1) * (Im2 z2))) - ((Im3 z1) * (Im3 z2))) + ((- (((((Rea z1) * (Im1 z2)) + ((Im1 z1) * (Rea z2))) + ((Im2 z1) * (Im3 z2))) - ((Im3 z1) * (Im2 z2)))) * <i>)) + ((- (((((Rea z1) * (Im2 z2)) + ((Im2 z1) * (Rea z2))) + ((Im3 z1) * (Im1 z2))) - ((Im1 z1) * (Im3 z2)))) * <j>)) + ((- (((((Rea z1) * (Im3 z2)) + ((Im3 z1) * (Rea z2))) + ((Im1 z1) * (Im2 z2))) - ((Im2 z1) * (Im1 z2)))) * <k>)
by A4, QUATERNI:44
;
hence
(z1 * z2) *' = (z2 *') * (z1 *')
by A1, A2, A6, A5, A9; verum