0q = [*0 ,0 *] by ARYTM_0:def 7
.= [*0 ,0 ,0 ,0 *] by QUATERNI:91 ;
then A1: ( Rea 0q = 0 & Im1 0q = 0 & Im2 0q = 0 & Im3 0q = 0 ) by 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 th
.= [*0 ,0 *] by QUATERNI:91, A1
.= 0 by ARYTM_0:def 7 ;
hence 0q ^2 = 0 ; :: thesis: verum