theorem :: MONOID_0:58

( 1 is_a_unity_wrt multnat & multnat is uniquely-decomposable )