let G be non empty multMagma ; :: thesis: ( G is cancelable iff for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c )
thus ( G is cancelable implies for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c ) :: thesis: ( ( for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c ) implies G is cancelable )

proof

assume A1: for a, b, c being Element of G st ( H₂(G) . (a,b) = H₂(G) . (a,c) or H₂(G) . (b,a) = H₂(G) . (c,a) ) holds
b = c ; :: according to MONOID_0:def 8,MONOID_0:def 19 :: thesis: for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c
let a, b, c be Element of G; :: thesis: ( ( a * b = a * c or b * a = c * a ) implies b = c )
thus ( ( a * b = a * c or b * a = c * a ) implies b = c ) by A1; :: thesis: verum

end;

assume A2: for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds
b = c ; :: thesis: G is cancelable
let a be Element of G; :: according to MONOID_0:def 8,MONOID_0:def 19 :: thesis: for b, c being Element of the carrier of G st ( the multF of G . (a,b) = the multF of G . (a,c) or the multF of G . (b,a) = the multF of G . (c,a) ) holds
b = c
let b, c be Element of G; :: thesis: ( ( the multF of G . (a,b) = the multF of G . (a,c) or the multF of G . (b,a) = the multF of G . (c,a) ) implies b = c )
A3: ( b * a = H₂(G) . (b,a) & c * a = H₂(G) . (c,a) ) ;
( a * b = H₂(G) . (a,b) & a * c = H₂(G) . (a,c) ) ;
hence ( ( the multF of G . (a,b) = the multF of G . (a,c) or the multF of G . (b,a) = the multF of G . (c,a) ) implies b = c ) by A2, A3; :: thesis: verum