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;
A3: ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( 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 ) )

proof

set F = <*Df*>;
A4: dom <*Df*> = Seg 1 by FINSEQ_1:38;

A5: now :: thesis: for i, j being Nat st i in dom <*Df*> & j in dom <*Df*> & i <> j 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
A6: i in dom <*Df*> and
A7: ( j in dom <*Df*> & i <> j ) ; :: thesis: <*Df*> . i misses <*Df*> . j
i = 1 by A4, A6, FINSEQ_1:2, TARSKI:def 1;
hence <*Df*> . i misses <*Df*> . j by A4, A7, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;

A8: for n being Nat st n in dom <*Df*> holds
<*Df*> . n = Df

proof

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 A4, FINSEQ_1:2, TARSKI:def 1;
hence <*Df*> . n = Df by FINSEQ_1:40; :: thesis: verum

end;

reconsider F = <*Df*> as Finite_Sep_Sequence of S by A5, MESFUNC3:4;
take F ; :: thesis: ( dom f = union (rng F) & ( 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;
then A9: rng F = {(F . 1)} by FINSEQ_1:38;
1 in Seg 1 ;
then F . 1 = Df by A4, A8;
hence dom f = union (rng F) by A9, ZFMISC_1:25; :: 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

hereby :: thesis: verum

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;

end;

now :: thesis: for x being Element of X st x in dom f holds
|.(f . x).| < +infty

let x be Element of X; :: thesis: ( x in dom f implies |.(f . x).| < +infty )
A14: r in REAL by XREAL_0:def 1;
assume x in dom f ; :: thesis: |.(f . x).| < +infty
then A15: f . x = r by A2;
then -infty < f . x by XXREAL_0:12, A14;
then A16: - +infty < f . x by XXREAL_3:def 3;
f . x < +infty by A15, XXREAL_0:9, A14;
hence |.(f . x).| < +infty by A16, EXTREAL1:22; :: thesis: verum

end;

then f is real-valued by MESFUNC2:def 1;
hence f is_simple_func_in S by A3, MESFUNC2:def 4; :: thesis: verum