theorem Th17: :: RFUNCT_3:17

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