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 set 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 set 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 set 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 set 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 set 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 set 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;

now

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 f . x = R_EAL r by A2;
then ( -infty < f . x & f . x < +infty ) by XXREAL_0:9, XXREAL_0:12;
then ( - +infty < f . x & f . x < +infty ) by XXREAL_3:def 3;
hence |.(f . x).| < +infty by EXTREAL2:59; :: thesis: verum

end;

then A3: f is real-valued by MESFUNC2:def 1;
set F = <*Df*>;
A5: dom <*Df*> = Seg 1 by FINSEQ_1:55;
B4: 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 A5, FINSEQ_1:4, TARSKI:def 1;
hence <*Df*> . n = Df by FINSEQ_1:57; :: thesis: verum

end;

now

let i, j be Nat; :: thesis: ( i in dom <*Df*> & j in dom <*Df*> & i <> j implies <*Df*> . i misses <*Df*> . j )
assume A6: ( i in dom <*Df*> & j in dom <*Df*> & i <> j ) ; :: thesis: <*Df*> . i misses <*Df*> . j
then ( i = 1 & j = 1 ) by A5, FINSEQ_1:4, TARSKI:def 1;
hence <*Df*> . i misses <*Df*> . j by A6; :: thesis: verum

end;

then reconsider F = <*Df*> as Finite_Sep_Sequence of S by MESFUNC3:4;
1 in Seg 1 ;
then A7: F . 1 = Df by A5, B4;
F = <*(F . 1)*> by FINSEQ_1:57;
then rng F = {(F . 1)} by FINSEQ_1:55;
then 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 A8: ( n in dom F & x in F . n & y in F . n ) ; :: thesis: f . x = f . y
F . n = Df by A8, B4;
then ( f . x = R_EAL r & f . y = R_EAL r ) by A2, A8;
hence f . x = f . y ; :: thesis: verum

end;

hence f is_simple_func_in S by A3, X, MESFUNC2:def 5; :: thesis: verum