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