let z1 be quaternion number ; (<k> * z1) + (z1 * <k> ) = [*(- (2 * (Im3 z1))),0 ,0 ,(2 * (Rea z1))*]
set z = <k> ;
A1:
<k> * z1 = [*(- (Im3 z1)),(- (Im2 z1)),(Im1 z1),(Rea z1)*]
by QUATERN2:1, QUATERNI:31;
then A2:
( Im2 (<k> * z1) = Im1 z1 & Im3 (<k> * z1) = Rea z1 )
by QUATERNI:23;
A3:
z1 * <k> = [*(- (Im3 z1)),(Im2 z1),(- (Im1 z1)),(Rea z1)*]
by QUATERN2:1, QUATERNI:31;
then A4:
( Rea (z1 * <k> ) = - (Im3 z1) & Im1 (z1 * <k> ) = Im2 z1 )
by QUATERNI:23;
A5:
( Im2 (z1 * <k> ) = - (Im1 z1) & Im3 (z1 * <k> ) = Rea z1 )
by A3, QUATERNI:23;
( Rea (<k> * z1) = - (Im3 z1) & Im1 (<k> * z1) = - (Im2 z1) )
by A1, QUATERNI:23;
then
(z1 * <k> ) + (<k> * z1) = ((((- (Im3 z1)) + (- (Im3 z1))) + (((- (Im2 z1)) + (Im2 z1)) * <i> )) + (((Im1 z1) - (Im1 z1)) * <j> )) + (((Rea z1) + (Rea z1)) * <k> )
by A2, A4, A5, QUATERNI:def 22;
hence
(<k> * z1) + (z1 * <k> ) = [*(- (2 * (Im3 z1))),0 ,0 ,(2 * (Rea z1))*]
by QUATERN2:1; verum