theorem Th54: :: MONOID_0:54

the_unity_wrt the multF of <NAT,*> = 1