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