let A be set ; 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 ; for o being BinOp of D st o is invertible holds
(o,D) .: A is invertible
let o be BinOp of D; ( 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 )
; MONOID_0:def 5 (o,D) .: A is invertible
let f, g be Element of Funcs (A,D); MONOID_0:def 5 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 ;
( x in A implies ex c being Element of D st S1[x,c] )
assume
x in A
;
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
;
S1[x,r]
thus
S1[
x,
r]
by A3;
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 MONOID_1:sch 1(A2);
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 ;
( x in A implies ex c being Element of D st S2[x,c] )
assume
x in A
;
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
;
S2[x,l]
thus
S2[
x,
l]
by A6;
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 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
; ex b1 being Element of Funcs (A,D) st
( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (b1,f) = g )
take
h2
; ( ((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;
o .: (f,h1) = ((o,D) .: A) . (f,h1)
by Def2;
hence
((o,D) .: A) . (f,h1) = g
by A10, A9, A11, FUNCT_1:2; ((o,D) .: A) . (h2,f) = g
A13:
dom (o .: (h2,f)) = A
by FUNCT_2:def 1;
o .: (h2,f) = ((o,D) .: A) . (h2,f)
by Def2;
hence
((o,D) .: A) . (h2,f) = g
by A13, A9, A14, FUNCT_1:2; verum