let X be non empty set ; :: thesis:
let L be non empty add-associative addLoopStr ; :: thesis:
let f, g, h be Function of X,L; :: thesis:

let o be object ; :: thesis:
assume o in X ; :: thesis:
then reconsider x = o as Element of X ;
thus ((f '+' g) '+' h) . o = ((f '+' g) . x) + (h . x) by defp
.= ((f . x) + (g . x)) + (h . x) by defp
.= (f . x) + ((g . x) + (h . x)) by RLVECT_1:def 3
.= (f . x) + ((g '+' h) . x) by defp
.= (f '+' (g '+' h)) . o by defp ; :: thesis:

end;