theorem Th16: :: HAHNBAN1:18

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