theorem :: MONOID_0:47

( addnat = addreal || NAT & addnat = addint || NAT )