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