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₁[ set , set ] means o . (f . $1),$2 = g . $1;
A2: for x being set st x in A holds
ex c being Element of D st S₁[x,c]

proof

let x be set ; :: 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:7;
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 set st x in A holds
S₁[x,h1 . x] from MONOID_1:sch 1(A2);
defpred S₂[ set , set ] means o . $2,(f . $1) = g . $1;
A5: for x being set st x in A holds
ex c being Element of D st S₂[x,c]

proof

let x be set ; :: 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:7;
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 set 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

let x be set ; :: 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:28
.= 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:9; :: thesis: (o,D .: A) . h2,f = g
A13: dom (o .: h2,f) = A by FUNCT_2:def 1;

A14: now

let x be set ; :: 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:28
.= 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:9; :: thesis: verum