theorem Th18: :: RFUNCT_3:18

for D being non empty set holds addpfunc D is having_a_unity