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

proof

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

end;

assume A2: for a, b, c being Element of G st a * b = a * c holds
b = c ; :: thesis: G is left-cancelable
let a be Element of G; :: according to MONOID_0:def 6,MONOID_0:def 17 :: thesis: for b, c being Element of the carrier of G st the multF of G . a,b = the multF of G . a,c holds
b = c
let b, c be Element of G; :: thesis: ( the multF of G . a,b = the multF of G . a,c implies b = c )
( 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 implies b = c ) by A2; :: thesis: verum