theorem :: MONOID_0:56
<NAT,*,1> = multLoopStr(# NAT,multnat,1 #)