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₁( object ) -> R_eal = c;
defpred S₁[ object ] means $1 in A;
A4: for x being object st S₁[x] holds
H₁(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₁[x] ) ) ) & ( for x being object st x in dom f holds
f . x = H₁(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

proof

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;

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

now :: thesis: for i, j being Nat st i in dom F & j in dom F & i <> j holds
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;

then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4;

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

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;
then A20: f . x = c by A5;
y in dom f by A18, A19;
hence f . x = f . y by A5, A20; :: thesis: verum

end;

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