theorem :: MONOID_0:64

for D being set
for F being non empty unital SubStr of D *+^ holds the_unity_wrt the multF of F = {}