theorem Th40: :: MONOID_0:40

for N being non empty unital SubStr of <REAL,+> holds the_unity_wrt the multF of N = 0