( Rea (1q " ) = 1 & Im1 (1q " ) = 0 & Im2 (1q " ) = 0 & Im3 (1q " ) = 0 ) by QUATERNI:68, QUATERN2:27, QUATERNI:29;
then 1q " = [*1,0 ,0 ,0 *] by QUATERNI:24;
hence 1q " = 1q by QUATERNI:24, QUATERNI:29; :: thesis: verum