let X be non empty set ; :: thesis: for S being SigmaField of X
for A being Element of S
for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
let S be SigmaField of X; :: thesis: for A being Element of S
for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
let A be Element of S; :: thesis: for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
let r be Real; :: thesis: ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
defpred S₁[ set ] means $1 in A;
deffunc H₁( set ) -> Real = r;
A1: for x being set st S₁[x] holds
H₁(x) in REAL ;
consider f being PartFunc of X,REAL such that
A2: ( ( for x being set holds
( x in dom f iff ( x in X & S₁[x] ) ) ) & ( for x being set st x in dom f holds
f . x = H₁(x) ) ) from PARTFUN1:sch 3(A1);
take f ; :: thesis: ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds
f . x = r ) )
A3: A c= dom f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in dom f )
assume x in A ; :: thesis: x in dom f
hence x in dom f by A2; :: thesis: verum

end;

A4: dom f c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in A )
assume x in dom f ; :: thesis: x in A
hence x in A by A2; :: thesis: verum

end;

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 = <*(dom f)*>;
A5: rng <*(dom f)*> = {(dom f)} by FINSEQ_1:55;
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;

now

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

end;

then reconsider F = F as Finite_Sep_Sequence of S by 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 ) )
thus dom f = union (rng F) by A5, ZFMISC_1:31; :: 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
A9: n in dom F and
A10: x in F . n and
A11: y in F . n ; :: thesis: f . x = f . y
dom F = Seg 1 by FINSEQ_1:55;
then A12: n = 1 by A9, FINSEQ_1:4, TARSKI:def 1;
then x in dom f by A10, FINSEQ_1:57;
then A13: f . x = r by A2;
y in dom f by A11, A12, FINSEQ_1:57;
hence f . x = f . y by A2, A13; :: thesis: verum

end;

end;

hence f is_simple_func_in S by Def7; :: thesis: ( dom f = A & ( for x being set st x in A holds
f . x = r ) )
thus dom f = A by A4, A3, XBOOLE_0:def 10; :: thesis: for x being set st x in A holds
f . x = r
thus for x being set st x in A holds
f . x = r by A2, A3; :: thesis: verum