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;

A8: dom (c (#) f) = dom f by MESFUNC1:def 6;

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

then A7:
c (#) f is real-valued
by MESFUNC2:def 1;|.((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;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

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

hence
c (#) f is_simple_func_in S
by A8, A7, A2, MESFUNC2:def 4; :: thesis: verumfor 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;(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