theorem :: MONOID_0:46

<NAT,+,0> = multLoopStr(# NAT,addnat,0 #)