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