1q = [*jj,(In (0,REAL))*] by ARYTM_0:def 5
.= [*jj,0,0,0*] by QUATERNI:91 ;
then A1: - 1q = [*(- jj),(- 0),(- 0),(- 0)*] by QUATERN2:4;
then A2: ( Rea (- 1q) = - 1 & Im1 (- 1q) = 0 ) by QUATERNI:23;
A3: ( Im2 (- 1q) = 0 & Im3 (- 1q) = 0 ) by A1, 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 Th78
.= [*jj,(In (0,REAL))*] by A2, A3, QUATERNI:91
.= 1 by ARYTM_0:def 5 ;
hence (- 1q) ^2 = 1 ; :: thesis: verum