let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let A be Element of S; :: thesis:
let r be Real; :: thesis:
defpred S₁[ object ] means $1 in A;
deffunc H₁( object ) -> Real = r;
A1: for x being object st S₁[x] holds
H₁(x) in REAL by XREAL_0:def 1;
consider f being PartFunc of X,REAL such that
A2: ( ( 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(A1);
take f ; :: thesis:
A3: A c= dom f by A2;
A4: dom f c= A by A2;
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 ) )

set F = <*(dom f)*>;
A5: rng <*(dom f)*> = {(dom f)} by FINSEQ_1:38;
then rng <*(dom f)*> = {A} by A4, A3, XBOOLE_0:def 10;
then reconsider F = <*(dom f)*> as FinSequence of S by FINSEQ_1:def 4;

let i, j be Nat; :: thesis:
assume that
A6: i in dom F and
A7: ( j in dom F & i <> j ) ; :: thesis:
A8: dom F = Seg 1 by FINSEQ_1:38;
then i = 1 by A6, FINSEQ_1:2, TARSKI:def 1;
hence F . i misses F . j by A7, A8, FINSEQ_1:2, TARSKI:def 1; :: thesis:

end;

then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4;
take F ; :: thesis:
thus dom f = union (rng F) by A5, ZFMISC_1:25; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume that
A9: n in dom F and
A10: x in F . n and
A11: y in F . n ; :: thesis:
dom F = Seg 1 by FINSEQ_1:38;
then A12: n = 1 by A9, FINSEQ_1:2, TARSKI:def 1;
then x in dom f by A10, FINSEQ_1:40;
then A13: f . x = r by A2;
y in dom f by A11, A12, FINSEQ_1:40;
hence f . x = f . y by A2, A13; :: thesis:

end;

end;

hence f is_simple_func_in S ; :: thesis:
thus dom f = A by A4, A3; :: thesis:
thus for x being object st x in A holds
f . x = r by A2; :: thesis: