theorem Th8: :: RVSUM_1:8

addreal is having_an_inverseOp by Th7;