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

proof

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

end;

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