let K be non empty Abelian addLoopStr ; :: thesis: the addF of K is commutative

now :: thesis: for a, b being Element of K holds the addF of K . (a,b) = the addF of K . (b,a)

let a, b be Element of K; :: thesis: the addF of K . (a,b) = the addF of K . (b,a)
thus the addF of K . (a,b) = a + b
.= the addF of K . (b,a) by RLVECT_1:2 ; :: thesis: verum

end;

hence the addF of K is commutative by BINOP_1:def 2; :: thesis: verum