let G be non empty multMagma ; :: thesis: ( G is left-invertible iff for a, b being Element of G ex l being Element of G st l * a = b )
thus ( G is left-invertible implies for a, b being Element of G ex l being Element of G st l * a = b ) :: thesis: ( ( for a, b being Element of G ex l being Element of G st l * a = b ) implies G is left-invertible )

proof

assume A1: for a, b being Element of G ex l being Element of G st H₂(G) . (l,a) = b ; :: according to MONOID_0:def 3,MONOID_0:def 14 :: thesis: for a, b being Element of G ex l being Element of G st l * a = b
let a, b be Element of G; :: thesis: ex l being Element of G st l * a = b
consider l being Element of G such that
A2: H₂(G) . (l,a) = b by A1;
take l ; :: thesis: l * a = b
thus l * a = b by A2; :: thesis: verum

end;

assume A3: for a, b being Element of G ex l being Element of G st l * a = b ; :: thesis: G is left-invertible
let a be Element of G; :: according to MONOID_0:def 3,MONOID_0:def 14 :: thesis: for b being Element of the carrier of G ex l being Element of the carrier of G st the multF of G . (l,a) = b
let b be Element of G; :: thesis: ex l being Element of the carrier of G st the multF of G . (l,a) = b
consider l being Element of G such that
A4: l * a = b by A3;
take l ; :: thesis: the multF of G . (l,a) = b
thus the multF of G . (l,a) = b by A4; :: thesis: verum