A1: Rea (<i> " ) = 0 by QUATERNI:30, QUATERN2:27;
A2: Im1 (<i> " ) = - 1 by QUATERNI:30, QUATERN2:27, QUATERNI:69;
A3: Im2 (<i> " ) = 0 by QUATERNI:30, QUATERN2:27;
A4: Im3 (<i> " ) = 0 by QUATERNI:30, QUATERN2:27;
<i> " = [*(- 0 ),(- 1),(- 0 ),(- 0 )*] by A1, A2, A3, A4, QUATERNI:24
.= - [*0 ,1,0 ,0 *] by QUATERN2:4
.= - <i> by QUATERNI:def 6, Lmx ;
hence <i> " = - <i> ; :: thesis: verum