theorem Th15: :: HAHNBAN1:17

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