theorem :: ZMODLAT1:40

for V, W being non empty ModuleStr over INT.Ring
for f, g, h being FrForm of V,W holds (f + g) + h = f + (g + h)