let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let c be Real; :: thesis:
set g = c (#) f;
assume A1: f is_simple_func_in S ; :: thesis:
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;

let x be Element of X; :: thesis:
assume A5: x in dom (c (#) f) ; :: thesis:
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:

end;

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

let n be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume that
A9: n in dom G and
A10: x in G . n and
A11: y in G . n ; :: thesis:
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:

end;

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