let K be non empty add-associative addLoopStr ; :: thesis: the addF of K is associative

now

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

end;

hence the addF of K is associative by BINOP_1:def 3; :: thesis: verum