let G be addGroup; :: thesis: for a, b being Element of G holds
( a * b = a iff a + b = b + a )
let a, b be Element of G; :: thesis: ( a * b = a iff a + b = b + a )
thus ( a * b = a implies a + b = b + a ) :: thesis: ( a + b = b + a implies a * b = a )

proof

assume a * b = a ; :: thesis: a + b = b + a
then a = (- b) + (a + b) by RLVECT_1:def 3;
hence a + b = b + a by Th12; :: thesis: verum

end;

assume a + b = b + a ; :: thesis: a * b = a
then a = (- b) + (a + b) by Th12;
hence a * b = a by RLVECT_1:def 3; :: thesis: verum