theorem Th16: :: RFUNCT_3:16

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