let G be Group; :: thesis: for a, b being Element of G st G is commutative Group holds
a |^ b = a
let a, b be Element of G; :: thesis: ( G is commutative Group implies a |^ b = a )
assume G is commutative Group ; :: thesis: a |^ b = a
hence a |^ b = (a * (b ")) * b by Lm1
.= a by Th1 ;
:: thesis: verum