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_{1}, b_{2} being Element of Funcs (A,D) st

( ((o,D) .: A) . (f,b_{1}) = g & ((o,D) .: A) . (b_{2},f) = g )

defpred S_{1}[ 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_{1}[x,c]

A4: for x being object st x in A holds

S_{1}[x,h1 . x]
from MONOID_1:sch 1(A2);

defpred S_{2}[ 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_{2}[x,c]

A7: for x being object st x in A holds

S_{2}[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_{1} being Element of Funcs (A,D) st

( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (b_{1},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;

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;

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

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

( ((o,D) .: A) . (f,b

defpred S

A2: for x being object st x in A holds

ex c being Element of D st S

proof

consider h1 being Function of A,D such that
let x be object ; :: thesis: ( x in A implies ex c being Element of D st S_{1}[x,c] )

assume x in A ; :: thesis: ex c being Element of D st S_{1}[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_{1}[x,r]

thus S_{1}[x,r]
by A3; :: thesis: verum

end;assume x in A ; :: thesis: ex c being Element of D st S

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

thus S

A4: for x being object st x in A holds

S

defpred S

A5: for x being object st x in A holds

ex c being Element of D st S

proof

consider h2 being Function of A,D such that
let x be object ; :: thesis: ( x in A implies ex c being Element of D st S_{2}[x,c] )

assume x in A ; :: thesis: ex c being Element of D st S_{2}[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_{2}[x,l]

thus S_{2}[x,l]
by A6; :: thesis: verum

end;assume x in A ; :: thesis: ex c being Element of D st S

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

thus S

A7: for x being object st x in A holds

S

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

( ((o,D) .: A) . (f,h1) = g & ((o,D) .: A) . (b

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

o .: (f,h1) = ((o,D) .: A) . (f,h1)
by Def2;(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;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

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

o .: (h2,f) = ((o,D) .: A) . (h2,f)
by Def2;(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;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

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