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;
set F = <*Df*>;
A3: dom <*Df*> = Seg 1 by FINSEQ_1:38;

A4: 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
A5: i in dom <*Df*> and
A6: j in dom <*Df*> and
A7: i <> j ; :: thesis: <*Df*> . i misses <*Df*> . j
i = 1 by A3, A5, FINSEQ_1:2, TARSKI:def 1;
hence <*Df*> . i misses <*Df*> . j by A3, A6, 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 A3, FINSEQ_1:2, TARSKI:def 1;
hence <*Df*> . n = Df ; :: thesis: verum

end;

reconsider F = <*Df*> as Finite_Sep_Sequence of S by A4, MESFUNC3:4;

A9: 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
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;

A14: rng F = {(F . 1)} by FINSEQ_1:38;
A15: r in REAL by XREAL_0:def 1;

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 )
assume x in dom f ; :: thesis: |.(f . x).| < +infty
then A16: f . x = r by A2;
then -infty < f . x by XXREAL_0:12, A15;
then A17: - +infty < f . x by XXREAL_3:def 3;
f . x < +infty by A16, XXREAL_0:9, A15;
hence |.(f . x).| < +infty by A17, EXTREAL1:22; :: thesis: verum

end;

then A18: f is real-valued by MESFUNC2:def 1;
dom f = union (rng F) by A14, ZFMISC_1:25;
hence f is_simple_func_in S by A18, A9, MESFUNC2:def 4; :: thesis: verum