let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let r be Real; :: thesis:
assume that
A1: dom f in S and
A2: for x being object st x in dom f holds
f . x = r ; :: thesis:
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:

let i, j be Nat; :: thesis:
assume that
A6: i in dom <*Df*> and
A7: ( j in dom <*Df*> & i <> j ) ; :: thesis:
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:

end;

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

proof

let n be Nat; :: thesis:
assume n in dom <*Df*> ; :: thesis:
then n = 1 by A4, FINSEQ_1:2, TARSKI:def 1;
hence <*Df*> . n = Df by FINSEQ_1:40; :: thesis:

end;

reconsider F = <*Df*> as Finite_Sep_Sequence of S by A5, MESFUNC3:4;
take F ; :: thesis:
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:

hereby :: thesis:

let n be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume that
A10: n in dom F and
A11: x in F . n and
A12: y in F . n ; :: thesis:
A13: F . n = Df by A8, A10;
then f . x = r by A2, A11;
hence f . x = f . y by A2, A12, A13; :: thesis:

end;

end;

now :: thesis:

let x be Element of X; :: thesis:
A14: r in REAL by XREAL_0:def 1;
assume x in dom f ; :: thesis:
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:

end;

then f is V75() by MESFUNC2:def 1;
hence f is_simple_func_in S by A3, MESFUNC2:def 4; :: thesis: