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 st f is_simple_func_in S holds

f is_simple_func_in COM (S,M)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

f is_simple_func_in COM (S,M)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

f is_simple_func_in COM (S,M)

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies f is_simple_func_in COM (S,M) )

assume A1: f is_simple_func_in S ; :: thesis: f is_simple_func_in COM (S,M)

then A2: f is V55() by MESFUNC2:def 4;

consider F being Finite_Sep_Sequence of S such that

A3: dom f = union (rng F) and

A4: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y by A1, MESFUNC2:def 4;

reconsider F1 = F as Finite_Sep_Sequence of COM (S,M) by Th32;

dom f = union (rng F1) by A3;

hence f is_simple_func_in COM (S,M) by A2, A4, MESFUNC2:def 4; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

f is_simple_func_in COM (S,M)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

f is_simple_func_in COM (S,M)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds

f is_simple_func_in COM (S,M)

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies f is_simple_func_in COM (S,M) )

assume A1: f is_simple_func_in S ; :: thesis: f is_simple_func_in COM (S,M)

then A2: f is V55() by MESFUNC2:def 4;

consider F being Finite_Sep_Sequence of S such that

A3: dom f = union (rng F) and

A4: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y by A1, MESFUNC2:def 4;

reconsider F1 = F as Finite_Sep_Sequence of COM (S,M) by Th32;

dom f = union (rng F1) by A3;

hence f is_simple_func_in COM (S,M) by A2, A4, MESFUNC2:def 4; :: thesis: verum