let A be set ; for D being non empty set
for o being BinOp of D st o is cancelable holds
(o,D) .: A is cancelable
let D be non empty set ; for o being BinOp of D st o is cancelable holds
(o,D) .: A is cancelable
let o be BinOp of D; ( o is cancelable implies (o,D) .: A is cancelable )
assume A1:
for a, b, c being Element of D st ( o . (a,b) = o . (a,c) or o . (b,a) = o . (c,a) ) holds
b = c
; MONOID_0:def 8 (o,D) .: A is cancelable
let f, g, h be Element of Funcs (A,D); MONOID_0:def 8 ( ( not ((o,D) .: A) . (f,g) = ((o,D) .: A) . (f,h) & not ((o,D) .: A) . (g,f) = ((o,D) .: A) . (h,f) ) or g = h )
assume A2:
( ((o,D) .: A) . (f,g) = ((o,D) .: A) . (f,h) or ((o,D) .: A) . (g,f) = ((o,D) .: A) . (h,f) )
; g = h
A3:
( A = dom (o .: (g,f)) & A = dom (o .: (h,f)) )
by FUNCT_2:def 1;
A4:
( ((o,D) .: A) . (f,h) = o .: (f,h) & ((o,D) .: A) . (h,f) = o .: (h,f) )
by Def2;
A5:
( A = dom (o .: (f,g)) & A = dom (o .: (f,h)) )
by FUNCT_2:def 1;
A6:
( ((o,D) .: A) . (f,g) = o .: (f,g) & ((o,D) .: A) . (g,f) = o .: (g,f) )
by Def2;
A7:
now for x being object st x in A holds
g . x = h . xlet x be
object ;
( x in A implies g . x = h . x )assume A8:
x in A
;
g . x = h . xthen reconsider a =
f . x,
b =
g . x,
c =
h . x as
Element of
D by FUNCT_2:5;
A9:
(
(o .: (g,f)) . x = o . (
b,
a) &
(o .: (h,f)) . x = o . (
c,
a) )
by A3, A8, FUNCOP_1:22;
(
(o .: (f,g)) . x = o . (
a,
b) &
(o .: (f,h)) . x = o . (
a,
c) )
by A5, A8, FUNCOP_1:22;
hence
g . x = h . x
by A1, A2, A6, A4, A9;
verum end;
( dom g = A & dom h = A )
by FUNCT_2:def 1;
hence
g = h
by A7, FUNCT_1:2; verum