let D be non empty set ; :: thesis: for f being BinOp of D holds
( f is invertible iff ( f is left-invertible & f is right-invertible ) )
let f be BinOp of D; :: thesis: ( f is invertible iff ( f is left-invertible & f is right-invertible ) )
thus ( f is invertible implies ( f is left-invertible & f is right-invertible ) ) :: thesis: ( f is left-invertible & f is right-invertible implies f is invertible )

proof

assume A1: for a, b being Element of D ex r, l being Element of D st
( f . a,r = b & f . l,a = b ) ; :: according to MONOID_0:def 5 :: thesis: ( f is left-invertible & f is right-invertible )

now

let a, b be Element of D; :: thesis: ex l being Element of D st f . l,a = b
consider r, l being Element of D such that
A2: ( f . a,r = b & f . l,a = b ) by A1;
take l = l; :: thesis: f . l,a = b
thus f . l,a = b by A2; :: thesis: verum

end;

hence for a, b being Element of D ex l being Element of D st f . l,a = b ; :: according to MONOID_0:def 3 :: thesis: f is right-invertible
let a, b be Element of D; :: according to MONOID_0:def 4 :: thesis: ex r being Element of D st f . a,r = b
consider r, l being Element of D such that
A3: ( f . a,r = b & f . l,a = b ) by A1;
take r ; :: thesis: f . a,r = b
thus f . a,r = b by A3; :: thesis: verum

end;

assume that
A4: for a, b being Element of D ex l being Element of D st f . l,a = b and
A5: for a, b being Element of D ex r being Element of D st f . a,r = b ; :: according to MONOID_0:def 3,MONOID_0:def 4 :: thesis: f is invertible
let a, b be Element of D; :: according to MONOID_0:def 5 :: thesis: ex r, l being Element of D st
( f . a,r = b & f . l,a = b )
consider l being Element of D such that
A6: f . l,a = b by A4;
consider r being Element of D such that
A7: f . a,r = b by A5;
take r ; :: thesis: ex l being Element of D st
( f . a,r = b & f . l,a = b )
take l ; :: thesis: ( f . a,r = b & f . l,a = b )
thus ( f . a,r = b & f . l,a = b ) by A6, A7; :: thesis: verum