theorem :: MONOID_0:48

( 0 is_a_unity_wrt addnat & addnat is uniquely-decomposable )