:: deftheorem defines <j> QUATERNI:def 3 :
<j> = (0,1,2,3) --> (0,0,1,0);