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 r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

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 r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

f is_simple_func_in S

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

for r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

f is_simple_func_in S

let f be PartFunc of X,ExtREAL; :: thesis: for r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

f is_simple_func_in S

let r be Real; :: thesis: ( dom f in S & ( for x being object st x in dom f holds

f . x = r ) implies f is_simple_func_in S )

assume that

A1: dom f in S and

A2: for x being object st x in dom f holds

f . x = r ; :: thesis: f is_simple_func_in S

reconsider Df = dom f as Element of S by A1;

set F = <*Df*>;

A3: dom <*Df*> = Seg 1 by FINSEQ_1:38;

<*Df*> . n = Df

then A14: rng F = {(F . 1)} by FINSEQ_1:38;

A15: r in REAL by XREAL_0:def 1;

1 in Seg 1 ;

then F . 1 = Df by A3, A8;

then dom f = union (rng F) by A14, ZFMISC_1:25;

hence f is_simple_func_in S by A18, A9, MESFUNC2:def 4; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

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 r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

f is_simple_func_in S

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

for r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

f is_simple_func_in S

let f be PartFunc of X,ExtREAL; :: thesis: for r being Real st dom f in S & ( for x being object st x in dom f holds

f . x = r ) holds

f is_simple_func_in S

let r be Real; :: thesis: ( dom f in S & ( for x being object st x in dom f holds

f . x = r ) implies f is_simple_func_in S )

assume that

A1: dom f in S and

A2: for x being object st x in dom f holds

f . x = r ; :: thesis: f is_simple_func_in S

reconsider Df = dom f as Element of S by A1;

set F = <*Df*>;

A3: dom <*Df*> = Seg 1 by FINSEQ_1:38;

A4: now :: thesis: for i, j being Nat st i in dom <*Df*> & j in dom <*Df*> & i <> j holds

<*Df*> . i misses <*Df*> . j

A8:
for n being Nat st n in dom <*Df*> holds <*Df*> . i misses <*Df*> . j

let i, j be Nat; :: thesis: ( i in dom <*Df*> & j in dom <*Df*> & i <> j implies <*Df*> . i misses <*Df*> . j )

assume that

A5: i in dom <*Df*> and

A6: j in dom <*Df*> and

A7: i <> j ; :: thesis: <*Df*> . i misses <*Df*> . j

i = 1 by A3, A5, FINSEQ_1:2, TARSKI:def 1;

hence <*Df*> . i misses <*Df*> . j by A3, A6, A7, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;assume that

A5: i in dom <*Df*> and

A6: j in dom <*Df*> and

A7: i <> j ; :: thesis: <*Df*> . i misses <*Df*> . j

i = 1 by A3, A5, FINSEQ_1:2, TARSKI:def 1;

hence <*Df*> . i misses <*Df*> . j by A3, A6, A7, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

<*Df*> . n = Df

proof

reconsider F = <*Df*> as Finite_Sep_Sequence of S by A4, MESFUNC3:4;
let n be Nat; :: thesis: ( n in dom <*Df*> implies <*Df*> . n = Df )

assume n in dom <*Df*> ; :: thesis: <*Df*> . n = Df

then n = 1 by A3, FINSEQ_1:2, TARSKI:def 1;

hence <*Df*> . n = Df by FINSEQ_1:40; :: thesis: verum

end;assume n in dom <*Df*> ; :: thesis: <*Df*> . n = Df

then n = 1 by A3, FINSEQ_1:2, TARSKI:def 1;

hence <*Df*> . n = Df by FINSEQ_1:40; :: thesis: verum

A9: now :: thesis: 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

F = <*(F . 1)*>
by FINSEQ_1:40;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

let n be Nat; :: thesis: 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

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )

assume that

A10: n in dom F and

A11: x in F . n and

A12: y in F . n ; :: thesis: f . x = f . y

A13: F . n = Df by A8, A10;

then f . x = r by A2, A11;

hence f . x = f . y by A2, A12, A13; :: thesis: verum

end;f . x = f . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )

assume that

A10: n in dom F and

A11: x in F . n and

A12: y in F . n ; :: thesis: f . x = f . y

A13: F . n = Df by A8, A10;

then f . x = r by A2, A11;

hence f . x = f . y by A2, A12, A13; :: thesis: verum

then A14: rng F = {(F . 1)} by FINSEQ_1:38;

A15: r in REAL by XREAL_0:def 1;

now :: thesis: for x being Element of X st x in dom f holds

|.(f . x).| < +infty

then A18:
f is real-valued
by MESFUNC2:def 1;|.(f . x).| < +infty

let x be Element of X; :: thesis: ( x in dom f implies |.(f . x).| < +infty )

assume x in dom f ; :: thesis: |.(f . x).| < +infty

then A16: f . x = r by A2;

then -infty < f . x by XXREAL_0:12, A15;

then A17: - +infty < f . x by XXREAL_3:def 3;

f . x < +infty by A16, XXREAL_0:9, A15;

hence |.(f . x).| < +infty by A17, EXTREAL1:22; :: thesis: verum

end;assume x in dom f ; :: thesis: |.(f . x).| < +infty

then A16: f . x = r by A2;

then -infty < f . x by XXREAL_0:12, A15;

then A17: - +infty < f . x by XXREAL_3:def 3;

f . x < +infty by A16, XXREAL_0:9, A15;

hence |.(f . x).| < +infty by A17, EXTREAL1:22; :: thesis: verum

1 in Seg 1 ;

then F . 1 = Df by A3, A8;

then dom f = union (rng F) by A14, ZFMISC_1:25;

hence f is_simple_func_in S by A18, A9, MESFUNC2:def 4; :: thesis: verum