let K be non empty add-associative addLoopStr ; :: thesis: for V being non empty ModuleStr over K
for f, g, h being Functional of V holds (f + g) + h = f + (g + h)
let V be non empty ModuleStr over K; :: thesis: for f, g, h being Functional of V holds (f + g) + h = f + (g + h)
let f, g, h be Functional of V; :: thesis: (f + g) + h = f + (g + h)

now :: thesis: for x being Element of V holds ((f + g) + h) . x = (f + (g + h)) . x

let x be Element of V; :: thesis: ((f + g) + h) . x = (f + (g + h)) . x
thus ((f + g) + h) . x = ((f + g) . x) + (h . x) by Def3
.= ((f . x) + (g . x)) + (h . x) by Def3
.= (f . x) + ((g . x) + (h . x)) by RLVECT_1:def 3
.= (f . x) + ((g + h) . x) by Def3
.= (f + (g + h)) . x by Def3 ; :: thesis: verum

end;

hence (f + g) + h = f + (g + h) by FUNCT_2:63; :: thesis: verum