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 b₁, b₂ being Element of Funcs (A,D) st
( ((o,D) .: A) . (f,b₁) = g & ((o,D) .: A) . (b₂,f) = g )
defpred S₁[ 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 S₁[x,c]

proof

let x be object ; :: thesis: ( x in A implies ex c being Element of D st S₁[x,c] )
assume x in A ; :: thesis: ex c being Element of D st S₁[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: S₁[x,r]
thus S₁[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
S₁[x,h1 . x] from MONOID_1:sch 1(A2);
defpred S₂[ 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 S₂[x,c]

proof

let x be object ; :: thesis: ( x in A implies ex c being Element of D st S₂[x,c] )
assume x in A ; :: thesis: ex c being Element of D st S₂[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: S₂[x,l]
thus S₂[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
S₂[x,h2 . x] from MONOID_1:sch 1(A5);
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 A8, FUNCT_2:def 2;
take h1 ; :: thesis: ex b₁ being Element of Funcs (A,D) st
( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (b₁,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 A10, FUNCOP_1:22
.= g . x by A4, A12 ;
:: thesis: verum

end;

o .: (f,h1) = ((o,D) .: A) . (f,h1) by Def2;
hence ((o,D) .: A) . (f,h1) = g by A10, A9, A11, FUNCT_1:2; :: 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 A13, FUNCOP_1:22
.= g . x by A7, A15 ;
:: thesis: verum

end;

o .: (h2,f) = ((o,D) .: A) . (h2,f) by Def2;
hence ((o,D) .: A) . (h2,f) = g by A13, A9, A14, FUNCT_1:2; :: thesis: verum