:: deftheorem defines multnat MONOID_0:def 33 :
multnat = the multF of <NAT,*>;