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;

A7: now

let x be set ; :: 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:7;
A9: ( (o .: g,f) . x = o . b,a & (o .: h,f) . x = o . c,a ) by A3, A8, FUNCOP_1:28;
( (o .: f,g) . x = o . a,b & (o .: f,h) . x = o . a,c ) by A5, A8, FUNCOP_1:28;
hence g . x = h . x by A1, A2, A6, A4, A9; :: thesis: verum

end;

( dom g = A & dom h = A ) by FUNCT_2:def 1;
hence g = h by A7, FUNCT_1:9; :: thesis: verum