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