theorem :: MONOID_0:8

for G being non empty multMagma holds
( G is left-invertible iff for a, b being Element of G ex l being Element of G st l * a = b )