theorem Th52: :: SEQ_4:52

the_inverseOp_wrt addcomplex = compcomplex by Th50, Th51, FINSEQOP:def 3;