1q = [*1,0 *] by ARYTM_0:def 7
.= [*1,0 ,0 ,0 *] by QUATERNI:91 ;
then - 1q = [*(- 1),(- 0 ),(- 0 ),(- 0 )*] by QUATERN2:4;
then A1: ( Rea (- 1q ) = - 1 & Im1 (- 1q ) = 0 & Im2 (- 1q ) = 0 & Im3 (- 1q ) = 0 ) by QUATERNI:23;
(- 1q ) ^2 = [*(((((Rea (- 1q )) ^2 ) - ((Im1 (- 1q )) ^2 )) - ((Im2 (- 1q )) ^2 )) - ((Im3 (- 1q )) ^2 )),(2 * ((Rea (- 1q )) * (Im1 (- 1q )))),(2 * ((Rea (- 1q )) * (Im2 (- 1q )))),(2 * ((Rea (- 1q )) * (Im3 (- 1q ))))*] by th
.= [*1,0 *] by QUATERNI:91, A1
.= 1 by ARYTM_0:def 7 ;
hence (- 1q ) ^2 = 1 ; :: thesis: verum