let F be RealNormSpace; :: thesis:
let r be Real; :: thesis:
let L be LinearFunc of F; :: thesis:
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;

let p be Real; :: thesis:
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:

end;