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