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