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