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