let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let f be PartFunc of X,ExtREAL ; :: thesis: for c being Real st f is_simple_func_in S holds
c (#) f is_simple_func_in S
let c be Real; :: thesis: ( f is_simple_func_in S implies c (#) f is_simple_func_in S )
assume A1: f is_simple_func_in S ; :: thesis: c (#) f is_simple_func_in S
set g = c (#) f;
A2: dom (c (#) f) = dom f by MESFUNC1:def 6;
A3: f is real-valued by A1, MESFUNC2:def 5;

now

let x be Element of X; :: thesis: ( x in dom (c (#) f) implies |.((c (#) f) . x).| < +infty )
assume A4: x in dom (c (#) f) ; :: thesis: |.((c (#) f) . x).| < +infty
( (R_EAL c) * (f . x) <> +infty & (R_EAL c) * (f . x) <> -infty ) by A3;
then ( (c (#) f) . x <> +infty & (c (#) f) . x <> -infty ) by A4, MESFUNC1:def 6;
then ( -infty < (c (#) f) . x & (c (#) f) . x < +infty ) by XXREAL_0:4, XXREAL_0:6;
then ( - +infty < (c (#) f) . x & (c (#) f) . x < +infty ) by XXREAL_3:def 3;
hence |.((c (#) f) . x).| < +infty by EXTREAL2:59; :: thesis: verum

end;

then A5: c (#) f is real-valued by MESFUNC2:def 1;
consider G being Finite_Sep_Sequence of S such that
A6: dom f = union (rng G) and
A7: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
f . x = f . y by A1, MESFUNC2:def 5;

now

let n be Nat; :: thesis: for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(c (#) f) . x = (c (#) f) . y
let x, y be Element of X; :: thesis: ( n in dom G & x in G . n & y in G . n implies (c (#) f) . x = (c (#) f) . y )
assume A8: ( n in dom G & x in G . n & y in G . n ) ; :: thesis: (c (#) f) . x = (c (#) f) . y
then G . n in rng G by FUNCT_1:12;
then ( x in dom (c (#) f) & y in dom (c (#) f) ) by A2, A6, A8, TARSKI:def 4;
then ( (c (#) f) . x = (R_EAL c) * (f . x) & (c (#) f) . y = (R_EAL c) * (f . y) ) by MESFUNC1:def 6;
hence (c (#) f) . x = (c (#) f) . y by A7, A8; :: thesis: verum

end;

hence c (#) f is_simple_func_in S by A2, A5, A6, MESFUNC2:def 5; :: thesis: verum