theorem Th15: :: RFUNCT_3:15

for D being non empty set holds addpfunc D is associative