theorem :: MONOID_0:46
<NAT,+,0> = multLoopStr(# NAT,addnat,0 #)