theorem Th15: :: MONOID_0:15

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 ) )