let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

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

for A being Element of S

for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

let M be sigma_Measure of S; :: thesis: for A being Element of S

for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

let A be Element of S; :: thesis: for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

let c be R_eal; :: thesis: ( c <> +infty & c <> -infty implies ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) ) )

assume that

A1: c <> +infty and

A2: c <> -infty ; :: thesis: ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

-infty < c by A2, XXREAL_0:6;

then A3: - +infty < c by XXREAL_3:def 3;

deffunc H_{1}( object ) -> R_eal = c;

defpred S_{1}[ object ] means $1 in A;

A4: for x being object st S_{1}[x] holds

H_{1}(x) in ExtREAL
;

consider f being PartFunc of X,ExtREAL such that

A5: ( ( for x being object holds

( x in dom f iff ( x in X & S_{1}[x] ) ) ) & ( for x being object st x in dom f holds

f . x = H_{1}(x) ) )
from PARTFUN1:sch 3(A4);

c < +infty by A1, XXREAL_0:4;

then |.c.| < +infty by A3, EXTREAL1:22;

then for x being Element of X st x in dom f holds

|.(f . x).| < +infty by A5;

then A6: f is real-valued by MESFUNC2:def 1;

take f ; :: thesis: ( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

A7: A c= dom f by A5;

set F = <*(dom f)*>;

A8: dom f c= A by A5;

A9: rng <*(dom f)*> = {(dom f)} by FINSEQ_1:38;

then A10: rng <*(dom f)*> = {A} by A8, A7, XBOOLE_0:def 10;

rng <*(dom f)*> c= S

hence f is_simple_func_in S by A6, A15, MESFUNC2:def 4; :: thesis: ( dom f = A & ( for x being object st x in A holds

f . x = c ) )

thus dom f = A by A8, A7; :: thesis: for x being object st x in A holds

f . x = c

thus for x being object st x in A holds

f . x = c by A5; :: thesis: verum

for M being sigma_Measure of S

for A being Element of S

for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

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

for A being Element of S

for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

let M be sigma_Measure of S; :: thesis: for A being Element of S

for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

let A be Element of S; :: thesis: for c being R_eal st c <> +infty & c <> -infty holds

ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

let c be R_eal; :: thesis: ( c <> +infty & c <> -infty implies ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) ) )

assume that

A1: c <> +infty and

A2: c <> -infty ; :: thesis: ex f being PartFunc of X,ExtREAL st

( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

-infty < c by A2, XXREAL_0:6;

then A3: - +infty < c by XXREAL_3:def 3;

deffunc H

defpred S

A4: for x being object st S

H

consider f being PartFunc of X,ExtREAL such that

A5: ( ( for x being object holds

( x in dom f iff ( x in X & S

f . x = H

c < +infty by A1, XXREAL_0:4;

then |.c.| < +infty by A3, EXTREAL1:22;

then for x being Element of X st x in dom f holds

|.(f . x).| < +infty by A5;

then A6: f is real-valued by MESFUNC2:def 1;

take f ; :: thesis: ( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds

f . x = c ) )

A7: A c= dom f by A5;

set F = <*(dom f)*>;

A8: dom f c= A by A5;

A9: rng <*(dom f)*> = {(dom f)} by FINSEQ_1:38;

then A10: rng <*(dom f)*> = {A} by A8, A7, XBOOLE_0:def 10;

rng <*(dom f)*> c= S

proof

then reconsider F = <*(dom f)*> as FinSequence of S by FINSEQ_1:def 4;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng <*(dom f)*> or z in S )

assume z in rng <*(dom f)*> ; :: thesis: z in S

then z = A by A10, TARSKI:def 1;

hence z in S ; :: thesis: verum

end;assume z in rng <*(dom f)*> ; :: thesis: z in S

then z = A by A10, TARSKI:def 1;

hence z in S ; :: thesis: verum

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

F . i misses F . j

then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4;F . i misses F . j

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

assume that

A11: i in dom F and

A12: j in dom F and

A13: i <> j ; :: thesis: F . i misses F . j

A14: dom F = Seg 1 by FINSEQ_1:38;

then i = 1 by A11, FINSEQ_1:2, TARSKI:def 1;

hence F . i misses F . j by A12, A13, A14, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;assume that

A11: i in dom F and

A12: j in dom F and

A13: i <> j ; :: thesis: F . i misses F . j

A14: dom F = Seg 1 by FINSEQ_1:38;

then i = 1 by A11, FINSEQ_1:2, TARSKI:def 1;

hence F . i misses F . j by A12, A13, A14, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

A15: 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

dom f = union (rng F)
by A9, ZFMISC_1:25;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

A16: n in dom F and

A17: x in F . n and

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

dom F = Seg 1 by FINSEQ_1:38;

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

then x in dom f by A17, FINSEQ_1:40;

then A20: f . x = c by A5;

y in dom f by A18, A19, FINSEQ_1:40;

hence f . x = f . y by A5, A20; :: 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

A16: n in dom F and

A17: x in F . n and

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

dom F = Seg 1 by FINSEQ_1:38;

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

then x in dom f by A17, FINSEQ_1:40;

then A20: f . x = c by A5;

y in dom f by A18, A19, FINSEQ_1:40;

hence f . x = f . y by A5, A20; :: thesis: verum

hence f is_simple_func_in S by A6, A15, MESFUNC2:def 4; :: thesis: ( dom f = A & ( for x being object st x in A holds

f . x = c ) )

thus dom f = A by A8, A7; :: thesis: for x being object st x in A holds

f . x = c

thus for x being object st x in A holds

f . x = c by A5; :: thesis: verum