let n, m be 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 A1: f = g ; :: thesis: r (#) f = r * g
( 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 9;
dom f = REAL m by FUNCT_2:def 1;
then A2: dom f = dom rG by FUNCT_2:def 1;
A3: r (#) f = f [#] r by INTEGR15:def 11;
for c being object st c in dom rG holds
rG . c = r (#) (f . c)
proof
let c be object ; :: thesis: ( c in dom rG implies rG . c = r (#) (f . c) )
assume A4: c in dom rG ; :: thesis: rG . c = r (#) (f . c)
then reconsider x = c as VECTOR of (REAL-NS m) by REAL_NS1:def 4;
reconsider c1 = c as Element of REAL m by A4;
rG . x = r * (g . x) by LOPBAN_1:36;
hence rG . c = r * (f /. c1) by A1, REAL_NS1:3
.= r (#) (f . c) ;
:: thesis: verum
end;
hence r (#) f = r * g by A2, A3, VALUED_2:def 39; :: thesis: verum