theorem Th51: :: SEQ_4:51

addcomplex is having_an_inverseOp by Th50;