A1: Im3 (<k> " ) = - ((Im3 <k> ) / (|.<k> .| ^2 )) by QUATERN2:29
.= - 1 by QUATERNI:31, QUATERNI:71 ;
A2: Im2 (<k> " ) = - ((Im2 <k> ) / (|.<k> .| ^2 )) by QUATERN2:29
.= 0 by QUATERNI:31 ;
A3: Im1 (<k> " ) = - ((Im1 <k> ) / (|.<k> .| ^2 )) by QUATERN2:29
.= 0 by QUATERNI:31 ;
Rea (<k> " ) = (Rea <k> ) / (|.<k> .| ^2 ) by QUATERN2:29
.= 0 by QUATERNI:31 ;
then <k> " = [*(- 0 ),(- 0 ),(- 0 ),(- 1)*] by A3, A2, A1, QUATERNI:24
.= - <k> by QUATERN2:4 ;
hence <k> " = - <k> ; :: thesis: verum