:: deftheorem defines op1 FUNCT_5:def 5 :
op1 = 0 .--> 0;