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 that
A2:
for a, b, c being Element of D st f . a,b = f . a,c holds
b = c
and
A3:
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
thus
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
by A2, A3; :: according to MONOID_0:def 8 :: thesis: verum