thus 0q = [*0 ,0 *] by ARYTM_0:def 7
.= [*0 ,0 ,0 ,0 *] by QUATERNI:def 6, QUATERNI:91 ; :: thesis: verum