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

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

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 3
.= 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