:: deftheorem defines <j> QUATERNI:def 10 :
<j> = [*0,0,1,0*];