let G be addGroup; :: thesis: ( ( for a, b being Element of G holds a * b = a ) implies G is Abelian )
assume A1: for a, b being Element of G holds a * b = a ; :: thesis: G is Abelian
let a be Element of G; :: according to RLVECT_1:def 2 :: 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