let A be set ; :: thesis: 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 ; :: thesis: for o being BinOp of D st o is cancelable holds

(o,D) .: A is cancelable

let o be BinOp of D; :: thesis: ( 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 ; :: according to MONOID_0:def 8 :: thesis: (o,D) .: A is cancelable

let f, g, h be Element of Funcs (A,D); :: according to MONOID_0:def 8 :: thesis: ( ( 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) ) ; :: thesis: 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;

hence g = h by A7, FUNCT_1:2; :: thesis: verum

for o being BinOp of D st o is cancelable holds

(o,D) .: A is cancelable

let D be non empty set ; :: thesis: for o being BinOp of D st o is cancelable holds

(o,D) .: A is cancelable

let o be BinOp of D; :: thesis: ( 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 ; :: according to MONOID_0:def 8 :: thesis: (o,D) .: A is cancelable

let f, g, h be Element of Funcs (A,D); :: according to MONOID_0:def 8 :: thesis: ( ( 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) ) ; :: thesis: 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 :: thesis: for x being object st x in A holds

g . x = h . x

( dom g = A & dom h = A )
by FUNCT_2:def 1;g . x = h . x

let x be object ; :: thesis: ( x in A implies g . x = h . x )

assume A8: x in A ; :: thesis: g . x = h . x

then 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; :: thesis: verum

end;assume A8: x in A ; :: thesis: g . x = h . x

then 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; :: thesis: verum

hence g = h by A7, FUNCT_1:2; :: thesis: verum