let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL
for r being Real st f is real-valued holds
r (#) f is real-valued
let f be PartFunc of C,ExtREAL ; :: thesis: for r being Real st f is real-valued holds
r (#) f is real-valued
let r be Real; :: thesis: ( f is real-valued implies r (#) f is real-valued )
assume A1: f is real-valued ; :: thesis: r (#) f is real-valued
A2: for x being Element of C st x in dom (r (#) f) holds
|.((r (#) f) . x).| < +infty

proof

let x be Element of C; :: thesis: ( x in dom (r (#) f) implies |.((r (#) f) . x).| < +infty )
assume A3: x in dom (r (#) f) ; :: thesis: |.((r (#) f) . x).| < +infty
A4: x in dom f by A3, MESFUNC1:def 6;
A5: |.(f . x).| < +infty by A1, A4, Def1;
A6: - +infty < f . x by A5, EXTREAL2:58;
A7: -infty < f . x by A6, XXREAL_3:def 3;
A8: f . x < +infty by A5, EXTREAL2:58;
reconsider y = f . x as Real by A7, A8, XXREAL_0:14;
A9: -infty < R_EAL (r * y) by XXREAL_0:12;
A10: R_EAL (r * y) < +infty by XXREAL_0:9;
A11: -infty < (R_EAL r) * (R_EAL y) by A9, EXTREAL1:38;
A12: (R_EAL r) * (R_EAL y) = (r (#) f) . x by A3, MESFUNC1:def 6;
A13: - +infty < (r (#) f) . x by A11, A12, XXREAL_3:def 3;
A14: (r (#) f) . x < +infty by A10, A12, EXTREAL1:38;
thus |.((r (#) f) . x).| < +infty by A13, A14, EXTREAL2:59; :: thesis: verum

end;

thus r (#) f is real-valued by A2, Def1; :: thesis: verum