let G be addGroup; :: thesis: for a, b, g being Element of G st a * g = b * g holds
a = b
let a, b, g be Element of G; :: thesis: ( a * g = b * g implies a = b )
assume a * g = b * g ; :: thesis: a = b
then (- g) + a = (- g) + b by Th6;
hence a = b by Th6; :: thesis: verum