let z1 be Quaternion; :: thesis: (<i> * z1) - (z1 * <i>) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*]
set z = <i> ;
set s = (<i> * z1) - (z1 * <i>);
A1: ( Rea (z1 * <i>) = ((((Rea z1) * (Rea <i>)) - ((Im1 z1) * (Im1 <i>))) - ((Im2 z1) * (Im2 <i>))) - ((Im3 z1) * (Im3 <i>)) & Im1 (z1 * <i>) = ((((Rea z1) * (Im1 <i>)) + ((Im1 z1) * (Rea <i>))) + ((Im2 z1) * (Im3 <i>))) - ((Im3 z1) * (Im2 <i>)) & Im2 (z1 * <i>) = ((((Rea z1) * (Im2 <i>)) + ((Im2 z1) * (Rea <i>))) + ((Im3 z1) * (Im1 <i>))) - ((Im1 z1) * (Im3 <i>)) & Im3 (z1 * <i>) = ((((Rea z1) * (Im3 <i>)) + ((Im3 z1) * (Rea <i>))) + ((Im1 z1) * (Im2 <i>))) - ((Im2 z1) * (Im1 <i>)) ) by QUATERNI:97;
A2: ( Im2 (<i> * z1) = ((((Rea <i>) * (Im2 z1)) + ((Im2 <i>) * (Rea z1))) + ((Im3 <i>) * (Im1 z1))) - ((Im1 <i>) * (Im3 z1)) & Im3 (<i> * z1) = ((((Rea <i>) * (Im3 z1)) + ((Im3 <i>) * (Rea z1))) + ((Im1 <i>) * (Im2 z1))) - ((Im2 <i>) * (Im1 z1)) ) by QUATERNI:97;
( Rea (<i> * z1) = - (Im1 z1) & Im1 (<i> * z1) = Rea z1 ) by A1, QUATERNI:30, QUATERNI:97;
then A3: ( Rea ((<i> * z1) - (z1 * <i>)) = (- (Im1 z1)) - (- (Im1 z1)) & Im1 ((<i> * z1) - (z1 * <i>)) = (Rea z1) - (Rea z1) ) by A1, QUATERNI:30, QUATERNI:42;
( Im2 ((<i> * z1) - (z1 * <i>)) = (- (Im3 z1)) - (Im3 z1) & Im3 ((<i> * z1) - (z1 * <i>)) = (Im2 z1) - (- (Im2 z1)) ) by A2, A1, QUATERNI:30, QUATERNI:42;
hence (<i> * z1) - (z1 * <i>) = [*0,0,(- (2 * (Im3 z1))),(2 * (Im2 z1))*] by A3, QUATERNI:24; :: thesis: verum