let m, n be Element of NAT ; :: thesis: 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
let f be Function of (REAL m),(REAL n); :: thesis: 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
let g be Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n)); :: thesis: for r being Real st f = g holds
r (#) f = r * g
let r be Real; :: thesis: ( f = g implies r (#) f = r * g )
assume AS: f = g ; :: thesis: r (#) f = r * g
set RB = R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n);
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider rG = r * g as Function of (REAL m),(REAL n) by LOPBAN_1:def 10;
dom f = REAL m by FUNCT_2:def 1;
then P1: dom f = dom rG by FUNCT_2:def 1;
for c being Element of REAL m st c in dom rG holds
rG /. c = r * (f /. c)

proof

let c be Element of REAL m; :: thesis: ( c in dom rG implies rG /. c = r * (f /. c) )
assume c in dom rG ; :: thesis: rG /. c = r * (f /. c)
reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def 4;
rG /. c = r * (g . x) by LOPBAN_1:42;
hence rG /. c = r * (f /. c) by AS, REAL_NS1:3; :: thesis: verum

end;

hence r (#) f = r * g by P1, INTEGR15:def 11; :: thesis: verum