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