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