:: deftheorem defines <k> QUATERNI:def 11 :
<k> = [*0,0,0,1*];