theorem Th50: :: SEQ_4:50

compcomplex is_an_inverseOp_wrt addcomplex