let G be addGroup; :: thesis: ( G is Abelian addGroup iff the addF of G is commutative )
thus ( G is Abelian addGroup implies the addF of G is commutative ) :: thesis: ( the addF of G is commutative implies G is Abelian addGroup )

proof

assume A1: G is Abelian addGroup ; :: thesis: the addF of G is commutative
let a be Element of G; :: according to BINOP_1:def 2 :: thesis: for b₁ being Element of the carrier of G holds the addF of G . (a,b₁) = the addF of G . (b₁,a)
let b be Element of G; :: thesis: the addF of G . (a,b) = the addF of G . (b,a)
thus the addF of G . (a,b) = a + b
.= b + a by A1, Lm1
.= the addF of G . (b,a) ; :: thesis: verum

end;

assume A2: the addF of G is commutative ; :: thesis: G is Abelian addGroup
G is Abelian by A2;
hence G is Abelian addGroup ; :: thesis: verum