:: deftheorem defines op2 FUNCT_5:def 6 :
op2 = (0,0) :-> 0;