theorem Th60: :: MONOID_0:60

for D being set holds the_unity_wrt the multF of (D *+^) = {}