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 )
set g = c (#) f;
assume A1: f is_simple_func_in S ; :: thesis: c (#) f is_simple_func_in S
then consider G being Finite_Sep_Sequence of S such that
A2: dom f = union (rng G) and
A3: 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 MESFUNC2:def 4;
A4: f is real-valued by A1, MESFUNC2:def 4;

now :: thesis: for x being Element of X st x in dom (c (#) f) holds
|.((c (#) f) . x).| < +infty

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

end;

then A7: c (#) f is real-valued by MESFUNC2:def 1;
A8: dom (c (#) f) = dom f by MESFUNC1:def 6;

now :: thesis: 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
(c (#) f) . x = (c (#) f) . y

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 that
A9: n in dom G and
A10: x in G . n and
A11: y in G . n ; :: thesis: (c (#) f) . x = (c (#) f) . y
A12: G . n in rng G by A9, FUNCT_1:3;
then y in dom (c (#) f) by A8, A2, A11, TARSKI:def 4;
then A13: (c (#) f) . y = c * (f . y) by MESFUNC1:def 6;
x in dom (c (#) f) by A8, A2, A10, A12, TARSKI:def 4;
then (c (#) f) . x = c * (f . x) by MESFUNC1:def 6;
hence (c (#) f) . x = (c (#) f) . y by A3, A9, A10, A11, A13; :: thesis: verum

end;

hence c (#) f is_simple_func_in S by A8, A7, A2, MESFUNC2:def 4; :: thesis: verum