let G be addGroup; :: thesis: for a, b being Element of G st G is Abelian addGroup holds
a * b = a
let a, b be Element of G; :: thesis: ( G is Abelian addGroup implies a * b = a )
assume G is Abelian addGroup ; :: thesis: a * b = a
hence a * b = (a + (- b)) + b by Lm1
.= a by Th1 ;
:: thesis: verum