let A be set ; :: thesis: for D being non empty set
for o being BinOp of D st o is invertible holds
(o,D) .: A is invertible

let D be non empty set ; :: thesis: for o being BinOp of D st o is invertible holds
(o,D) .: A is invertible

let o be BinOp of D; :: thesis: ( o is invertible implies (o,D) .: A is invertible )
assume A1: for a, b being Element of D ex r, l being Element of D st
( o . (a,r) = b & o . (l,a) = b ) ; :: according to MONOID_0:def 5 :: thesis: (o,D) .: A is invertible
let f, g be Element of Funcs (A,D); :: according to MONOID_0:def 5 :: thesis: ex b1, b2 being Element of Funcs (A,D) st
( ((o,D) .: A) . (f,b1) = g & ((o,D) .: A) . (b2,f) = g )

defpred S1[ object , object ] means o . ((f . \$1),\$2) = g . \$1;
A2: for x being object st x in A holds
ex c being Element of D st S1[x,c]
proof
let x be object ; :: thesis: ( x in A implies ex c being Element of D st S1[x,c] )
assume x in A ; :: thesis: ex c being Element of D st S1[x,c]
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;
consider r, l being Element of D such that
A3: o . (a,r) = b and
o . (l,a) = b by A1;
take r ; :: thesis: S1[x,r]
thus S1[x,r] by A3; :: thesis: verum
end;
consider h1 being Function of A,D such that
A4: for x being object st x in A holds
S1[x,h1 . x] from defpred S2[ object , object ] means o . (\$2,(f . \$1)) = g . \$1;
A5: for x being object st x in A holds
ex c being Element of D st S2[x,c]
proof
let x be object ; :: thesis: ( x in A implies ex c being Element of D st S2[x,c] )
assume x in A ; :: thesis: ex c being Element of D st S2[x,c]
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:5;
consider r, l being Element of D such that
o . (a,r) = b and
A6: o . (l,a) = b by A1;
take l ; :: thesis: S2[x,l]
thus S2[x,l] by A6; :: thesis: verum
end;
consider h2 being Function of A,D such that
A7: for x being object st x in A holds
S2[x,h2 . x] from A8: ( dom h1 = A & dom h2 = A ) by FUNCT_2:def 1;
( rng h1 c= D & rng h2 c= D ) ;
then reconsider h1 = h1, h2 = h2 as Element of Funcs (A,D) by ;
take h1 ; :: thesis: ex b1 being Element of Funcs (A,D) st
( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (b1,f) = g )

take h2 ; :: thesis: ( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (h2,f) = g )
A9: dom g = A by FUNCT_2:def 1;
A10: dom (o .: (f,h1)) = A by FUNCT_2:def 1;
A11: now :: thesis: for x being object st x in A holds
(o .: (f,h1)) . x = g . x
let x be object ; :: thesis: ( x in A implies (o .: (f,h1)) . x = g . x )
assume A12: x in A ; :: thesis: (o .: (f,h1)) . x = g . x
hence (o .: (f,h1)) . x = o . ((f . x),(h1 . x)) by
.= g . x by ;
:: thesis: verum
end;
o .: (f,h1) = ((o,D) .: A) . (f,h1) by Def2;
hence ((o,D) .: A) . (f,h1) = g by ; :: thesis: ((o,D) .: A) . (h2,f) = g
A13: dom (o .: (h2,f)) = A by FUNCT_2:def 1;
A14: now :: thesis: for x being object st x in A holds
(o .: (h2,f)) . x = g . x
let x be object ; :: thesis: ( x in A implies (o .: (h2,f)) . x = g . x )
assume A15: x in A ; :: thesis: (o .: (h2,f)) . x = g . x
hence (o .: (h2,f)) . x = o . ((h2 . x),(f . x)) by
.= g . x by ;
:: thesis: verum
end;
o .: (h2,f) = ((o,D) .: A) . (h2,f) by Def2;
hence ((o,D) .: A) . (h2,f) = g by ; :: thesis: verum