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