for K being non empty right-distributive doubleLoopStr
for V, W being non empty ModuleStr over K
for a being Element of K
for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)