theorem Th9: :: RVSUM_1:9

the_inverseOp_wrt addreal = compreal by Th7, Th8, FINSEQOP:def 3;