theorem Th7: :: RVSUM_1:7

compreal is_an_inverseOp_wrt addreal