for K being non empty add-associative addLoopStr
for V, W being non empty ModuleStr over K
for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)