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 set 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 set 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 set 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 set 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 set st x in A holds
f . x = c ) ) )
assume A1: ( c <> +infty & c <> -infty ) ; :: thesis: ex f being PartFunc of X,ExtREAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = c ) )
defpred S₁[ set ] means $1 in A;
deffunc H₁( set ) -> R_eal = c;
A2: for x being set st S₁[x] holds
H₁(x) in ExtREAL ;
consider f being PartFunc of X,ExtREAL such that
A3: ( ( for x being set holds
( x in dom f iff ( x in X & S₁[x] ) ) ) & ( for x being set st x in dom f holds
f . x = H₁(x) ) ) from PARTFUN1:sch 3(A2);
take f ; :: thesis: ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = c ) )
( -infty < c & c < +infty ) by A1, XXREAL_0:4, XXREAL_0:6;
then ( - +infty < c & c < +infty ) by XXREAL_3:def 3;
then |.c.| < +infty by EXTREAL2:59;
then for x being Element of X st x in dom f holds
|.(f . x).| < +infty by A3;
then A4: f is real-valued by MESFUNC2:def 1;
A5: dom f c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in A )
assume x in dom f ; :: thesis: x in A
hence x in A by A3; :: thesis: verum

end;

A6: A c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in dom f )
assume x in A ; :: thesis: x in dom f
hence x in dom f by A3; :: thesis: verum

end;

set F = <*(dom f)*>;
A7: rng <*(dom f)*> = {(dom f)} by FINSEQ_1:55;
then A8: rng <*(dom f)*> = {A} by A5, A6, XBOOLE_0:def 10;
rng <*(dom f)*> c= S

proof

let z be set ; :: 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 A8, TARSKI:def 1;
hence z in S ; :: thesis: verum

end;

then reconsider F = <*(dom f)*> as FinSequence of S by FINSEQ_1:def 4;

now

let i, j be Nat; :: thesis: ( i in dom F & j in dom F & i <> j implies F . i misses F . j )
assume A9: ( i in dom F & j in dom F & i <> j ) ; :: thesis: F . i misses F . j
dom F = Seg 1 by FINSEQ_1:55;
then ( i = 1 & j = 1 ) by A9, FINSEQ_1:4, TARSKI:def 1;
hence F . i misses F . j by A9; :: thesis: verum

end;

then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4;
X: dom f = union (rng F) by A7, ZFMISC_1:31;

now

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 A10: ( n in dom F & x in F . n & y in F . n ) ; :: thesis: f . x = f . y
dom F = Seg 1 by FINSEQ_1:55;
then n = 1 by A10, FINSEQ_1:4, TARSKI:def 1;
then A11: ( x in dom f & y in dom f ) by A10, FINSEQ_1:57;
then f . x = c by A3;
hence f . x = f . y by A3, A11; :: thesis: verum

end;

hence f is_simple_func_in S by A4, X, MESFUNC2:def 5; :: thesis: ( dom f = A & ( for x being set st x in A holds
f . x = c ) )
thus dom f = A by A5, A6, XBOOLE_0:def 10; :: thesis: for x being set st x in A holds
f . x = c
thus for x being set st x in A holds
f . x = c by A3, A6; :: thesis: verum