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