for D being non empty set
for F being non empty SubStr of D *+^ st {} is Element of F holds
( F is unital & the_unity_wrt the multF of F = {} )