theorem Th9: :: PDIFF_6:9

for n, m being Nat
for f being Function of (REAL m),(REAL n)
for g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for r being Real st f = g holds
r (#) f = r * g