A1: 1q = [*jj,(In (0,REAL))*] by ARYTM_0:def 5
.= [*jj,0,0,0*] by QUATERNI:91 ;
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 ^3 = 1 ; :: thesis: verum