let r be Real; :: thesis: for L being LINEAR holds r (#) L is LINEAR
let L be LINEAR; :: thesis: r (#) L is LINEAR
consider g being Real such that
A1: for p being Real holds L . p = g * p by Def4;
A2: L is total by Def4;

now

let p be Real; :: thesis: (r (#) L) . p = (r * g) * p
thus (r (#) L) . p = r * (L . p) by A2, RFUNCT_1:57
.= r * (g * p) by A1
.= (r * g) * p ; :: thesis: verum

end;

hence r (#) L is LINEAR by A2, Def4; :: thesis: verum