theorem Th54: :: MONOID_0:54
the_unity_wrt the multF of <NAT,*> = 1