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

now

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:5 ; :: thesis: verum

end;

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