theorem Th4: :: NDIFF_3:4

for F being RealNormSpace
for r being Real
for L being LinearFunc of F holds r (#) L is LinearFunc of F