let r be Real; :: thesis: for L being LinearFunc holds r (#) L is LinearFunc
let L be LinearFunc; :: thesis: r (#) L is LinearFunc
consider g being Real such that
A1: for p being Real holds L . p = g * p by Def3;
A2: L is total by Def3;
now :: thesis: for p being Real holds (r (#) L) . p = (r * g) * p
let p be Real; :: thesis: (r (#) L) . p = (r * g) * p
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus (r (#) L) . p = r * (L . pp) by A2, RFUNCT_1:57
.= r * (g * p) by A1
.= (r * g) * p ; :: thesis: verum
end;
hence r (#) L is LinearFunc by A2, Def3; :: thesis: verum