A1: 1q = [*1,0 *] by ARYTM_0:def 7
.= [*1,0 ,0 ,0 *] by QUATERNI:91 ;
then A2: - 1q = [*(- 1),(- 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 Th82
.= [*1,0 *] by A3, A4, QUATERNI:91
.= 1 by ARYTM_0:def 7 ;
then (- 1q ) ^3 = - 1q by QUATERN2:15
.= [*(- 1),(- 0 ),(- 0 ),(- 0 )*] by A1, QUATERN2:4
.= [*(- 1),(- 0 )*] by QUATERNI:91
.= - 1 by ARYTM_0:def 7 ;
hence (- 1q ) ^3 = - 1 ; :: thesis: verum