theorem Th3: :: FDIFF_1:3

for r being Real
for L being LinearFunc holds r (#) L is LinearFunc