theorem Th14: :: RFUNCT_3:14

for D being non empty set holds addpfunc D is commutative