for D being non empty set holds the_unity_wrt (addpfunc D) = ([#] D) --> 0