let F be non trivial RealNormSpace; :: thesis: for r being Real
for L being LINEAR of F holds r (#) L is LINEAR of F
let r be Real; :: thesis: for L being LINEAR of F holds r (#) L is LINEAR of F
let L be LINEAR of F; :: thesis: r (#) L is LINEAR 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;
then A3: dom (r (#) L) = REAL by FUNCT_2:def 1;

now

let p be Real; :: thesis: (r (#) L) . p = p * (r * g)
thus (r (#) L) . p = (r (#) L) /. p by A3, PARTFUN1:def 6
.= r * (L /. p) 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 LINEAR of F by A2, Def2; :: thesis: verum