for G being non empty multMagma st G is associative holds
( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) )