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