theorem Th17: :: HAHNBAN1:19

for K being non empty associative multMagma
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 * (s * f)