let D be non empty set ; :: thesis: for f being BinOp of D holds
( f is cancelable iff ( f is left-cancelable & f is right-cancelable ) )
let f be BinOp of D; :: thesis: ( f is cancelable iff ( f is left-cancelable & f is right-cancelable ) )
thus ( f is cancelable implies ( f is left-cancelable & f is right-cancelable ) ) :: thesis: ( f is left-cancelable & f is right-cancelable implies f is cancelable )

proof

assume A1: for a, b, c being Element of D st ( f . a,b = f . a,c or f . b,a = f . c,a ) holds
b = c ; :: according to MONOID_0:def 8 :: thesis: ( f is left-cancelable & f is right-cancelable )
hence for a, b, c being Element of D st f . a,b = f . a,c holds
b = c ; :: according to MONOID_0:def 6 :: thesis: f is right-cancelable
thus for a, b, c being Element of D st f . b,a = f . c,a holds
b = c by A1; :: according to MONOID_0:def 7 :: thesis: verum

end;

assume ( ( for a, b, c being Element of D st f . a,b = f . a,c holds
b = c ) & ( for a, b, c being Element of D st f . b,a = f . c,a holds
b = c ) ) ; :: according to MONOID_0:def 6,MONOID_0:def 7 :: thesis: f is cancelable
hence for a, b, c being Element of D st ( f . a,b = f . a,c or f . b,a = f . c,a ) holds
b = c ; :: according to MONOID_0:def 8 :: thesis: verum