let z1 be Quaternion; (<k> * z1) + (z1 * <k>) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*]
set z = <k> ;
A1: <k> * z1 =
(((((((Rea <k>) * (Rea z1)) - ((Im1 <k>) * (Im1 z1))) - ((Im2 <k>) * (Im2 z1))) - ((Im3 <k>) * (Im3 z1))) + ((((((Rea <k>) * (Im1 z1)) + ((Im1 <k>) * (Rea z1))) + ((Im2 <k>) * (Im3 z1))) - ((Im3 <k>) * (Im2 z1))) * <i>)) + ((((((Rea <k>) * (Im2 z1)) + ((Im2 <k>) * (Rea z1))) + ((Im3 <k>) * (Im1 z1))) - ((Im1 <k>) * (Im3 z1))) * <j>)) + ((((((Rea <k>) * (Im3 z1)) + ((Im3 <k>) * (Rea z1))) + ((Im1 <k>) * (Im2 z1))) - ((Im2 <k>) * (Im1 z1))) * <k>)
by QUATERNI:93
.=
[*(- (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> =
(((((((Rea z1) * (Rea <k>)) - ((Im1 z1) * (Im1 <k>))) - ((Im2 z1) * (Im2 <k>))) - ((Im3 z1) * (Im3 <k>))) + ((((((Rea z1) * (Im1 <k>)) + ((Im1 z1) * (Rea <k>))) + ((Im2 z1) * (Im3 <k>))) - ((Im3 z1) * (Im2 <k>))) * <i>)) + ((((((Rea z1) * (Im2 <k>)) + ((Im2 z1) * (Rea <k>))) + ((Im3 z1) * (Im1 <k>))) - ((Im1 z1) * (Im3 <k>))) * <j>)) + ((((((Rea z1) * (Im3 <k>)) + ((Im3 z1) * (Rea <k>))) + ((Im1 z1) * (Im2 <k>))) - ((Im2 z1) * (Im1 <k>))) * <k>)
by QUATERNI:93
.=
[*(- (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:92;
hence
(<k> * z1) + (z1 * <k>) = [*(- (2 * (Im3 z1))),0,0,(2 * (Rea z1))*]
by QUATERN2:1; verum