theorem Th43: :: MONOID_0:43

<NAT,+> = multMagma(# NAT,addnat #) by Def27;