let G be Group; :: thesis: ( ( for a, b being Element of G holds a |^ b = a ) implies G is commutative )
assume A1: for a, b being Element of G holds a |^ b = a ; :: thesis: G is commutative
let a be Element of G; :: according to GROUP_1:def 12 :: thesis: for b₁ being Element of the carrier of G holds a * b₁ = b₁ * a
let b be Element of G; :: thesis: a * b = b * a
a |^ b = a by A1;
hence a * b = b * a by Th22; :: thesis: verum