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

proof

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

end;

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