A1: 0q = [*0 ,0 *] by ARYTM_0:def 7
.= [*0 ,0 ,0 ,0 *] by QUATERNI:91 ;
A2: ( Rea 0q = 0 & Im1 0q = 0 ) by A1, QUATERNI:23;
A3: ( Im2 0q = 0 & Im3 0q = 0 ) by A1, QUATERNI:23;
A4: 0q ^2 = [*(((((Rea 0q ) ^2 ) - ((Im1 0q ) ^2 )) - ((Im2 0q ) ^2 )) - ((Im3 0q ) ^2 )),(2 * ((Rea 0q ) * (Im1 0q ))),(2 * ((Rea 0q ) * (Im2 0q ))),(2 * ((Rea 0q ) * (Im3 0q )))*] by Th82
.= [*0 ,0 *] by A2, A3, QUATERNI:91
.= 0 by ARYTM_0:def 7 ;
thus 0q ^3 = 0 by A4; :: thesis: verum