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 ;
Rea (<i> ") = (Rea <i>) / (|.<i>.| ^2) by QUATERN2:29
.= 0 by QUATERNI:30 ;
then <i> " = [*(- 0),(- 1),(- 0),(- 0)*] by A3, A2, A1, QUATERNI:24
.= - [*0,jj,0,0*] by QUATERN2:4
.= - <i> by Lm2, QUATERNI:def 6 ;
hence <i> " = - <i> ; :: thesis: verum