let F be RealNormSpace; :: thesis: for r being Real
for L being LinearFunc of F holds r (#) L is LinearFunc of F
let r be Real; :: thesis: for L being LinearFunc of F holds r (#) L is LinearFunc of F
let L be LinearFunc of F; :: thesis: r (#) L is LinearFunc of F
consider g being Point of F such that
A1: for p being Real holds L /. p = p * g by Def2;
A2: r (#) L is total by VFUNCT_1:34;

now :: thesis: for p being Real holds (r (#) L) /. p = p * (r * g)

let p be Real; :: thesis: (r (#) L) /. p = p * (r * g)
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus (r (#) L) /. p = r * (L /. pp) by VFUNCT_1:39
.= r * (p * g) by A1
.= (r * p) * g by RLVECT_1:def 7
.= p * (r * g) by RLVECT_1:def 7 ; :: thesis: verum

end;

hence r (#) L is LinearFunc of F by A2, Def2; :: thesis: verum