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 A being Element of S st f is_simple_func_in S holds
f | A 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 A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let A be Element of S; :: thesis: ( f is_simple_func_in S implies f | A is_simple_func_in S )
assume A1: f is_simple_func_in S ; :: thesis: f | A is_simple_func_in S
then consider F being Finite_Sep_Sequence of S such that
A2: dom f = union (rng F) and
A3: 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 by MESFUNC2:def 4;
deffunc H₁( Nat) -> Element of bool X = (F . $1) /\ A;
consider G being FinSequence such that
A4: ( len G = len F & ( for n being Nat st n in dom G holds
G . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A5: rng G c= S

proof

let P be object ; :: according to TARSKI:def 3 :: thesis: ( not P in rng G or P in S )
assume P in rng G ; :: thesis: P in S
then consider k being Nat such that
A6: k in dom G and
A7: P = G . k by FINSEQ_2:10;
k in Seg (len F) by A4, A6, FINSEQ_1:def 3;
then k in dom F by FINSEQ_1:def 3;
then A8: F . k in rng F by FUNCT_1:3;
G . k = (F . k) /\ A by A4, A6;
hence P in S by A7, A8, FINSUB_1:def 2; :: thesis: verum

end;

A9: dom G = Seg (len F) by A4, FINSEQ_1:def 3;
reconsider G = G as FinSequence of S by A5, FINSEQ_1:def 4;
for i, j being Nat st i in dom G & j in dom G & i <> j holds
G . i misses G . j

proof

let i, j be Nat; :: thesis: ( i in dom G & j in dom G & i <> j implies G . i misses G . j )
assume that
A10: i in dom G and
A11: j in dom G and
A12: i <> j ; :: thesis: G . i misses G . j
j in Seg (len F) by A4, A11, FINSEQ_1:def 3;
then A13: j in dom F by FINSEQ_1:def 3;
i in Seg (len F) by A4, A10, FINSEQ_1:def 3;
then i in dom F by FINSEQ_1:def 3;
then A14: F . i misses F . j by A12, A13, MESFUNC3:4;
A15: G . j = (F . j) /\ A by A4, A11;
G . i = (F . i) /\ A by A4, A10;
then (G . i) /\ (G . j) = (((F . i) /\ A) /\ (F . j)) /\ A by A15, XBOOLE_1:16
.= (((F . i) /\ (F . j)) /\ A) /\ A by XBOOLE_1:16
.= ({} /\ A) /\ A by A14 ;
hence G . i misses G . j ; :: thesis: verum

end;

then reconsider G = G as Finite_Sep_Sequence of S by MESFUNC3:4;
for v being object st v in union (rng G) holds
v in dom (f | A)

proof

let v be object ; :: thesis: ( v in union (rng G) implies v in dom (f | A) )
assume v in union (rng G) ; :: thesis: v in dom (f | A)
then consider W being set such that
A16: v in W and
A17: W in rng G by TARSKI:def 4;
consider k being Nat such that
A18: k in dom G and
A19: W = G . k by A17, FINSEQ_2:10;
k in Seg (len F) by A4, A18, FINSEQ_1:def 3;
then k in dom F by FINSEQ_1:def 3;
then A20: F . k in rng F by FUNCT_1:3;
A21: G . k = (F . k) /\ A by A4, A18;
then v in F . k by A16, A19, XBOOLE_0:def 4;
then A22: v in union (rng F) by A20, TARSKI:def 4;
v in A by A16, A19, A21, XBOOLE_0:def 4;
then v in (dom f) /\ A by A2, A22, XBOOLE_0:def 4;
hence v in dom (f | A) by RELAT_1:61; :: thesis: verum

end;

then A23: union (rng G) c= dom (f | A) ;
for v being object st v in dom (f | A) holds
v in union (rng G)

proof

let v be object ; :: thesis: ( v in dom (f | A) implies v in union (rng G) )
assume v in dom (f | A) ; :: thesis: v in union (rng G)
then A24: v in (dom f) /\ A by RELAT_1:61;
then A25: v in A by XBOOLE_0:def 4;
v in dom f by A24, XBOOLE_0:def 4;
then consider W being set such that
A26: v in W and
A27: W in rng F by A2, TARSKI:def 4;
consider k being Nat such that
A28: k in dom F and
A29: W = F . k by A27, FINSEQ_2:10;
A30: k in Seg (len F) by A28, FINSEQ_1:def 3;
then k in dom G by A4, FINSEQ_1:def 3;
then A31: G . k in rng G by FUNCT_1:3;
G . k = (F . k) /\ A by A4, A9, A30;
then v in G . k by A25, A26, A29, XBOOLE_0:def 4;
hence v in union (rng G) by A31, TARSKI:def 4; :: thesis: verum

end;

then dom (f | A) c= union (rng G) ;
then A32: dom (f | A) = union (rng G) by A23;
A33: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | A) . x = (f | A) . y

proof

let n be Nat; :: thesis: for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | A) . x = (f | A) . y
let x, y be Element of X; :: thesis: ( n in dom G & x in G . n & y in G . n implies (f | A) . x = (f | A) . y )
assume that
A34: n in dom G and
A35: x in G . n and
A36: y in G . n ; :: thesis: (f | A) . x = (f | A) . y
A37: G . n in rng G by A34, FUNCT_1:3;
then A38: x in dom (f | A) by A32, A35, TARSKI:def 4;
A39: G . n = (F . n) /\ A by A4, A34;
then A40: y in F . n by A36, XBOOLE_0:def 4;
n in Seg (len F) by A4, A34, FINSEQ_1:def 3;
then A41: n in dom F by FINSEQ_1:def 3;
x in F . n by A35, A39, XBOOLE_0:def 4;
then f . x = f . y by A3, A40, A41;
then A42: (f | A) . x = f . y by A38, FUNCT_1:47;
y in dom (f | A) by A32, A36, A37, TARSKI:def 4;
hence (f | A) . x = (f | A) . y by A42, FUNCT_1:47; :: thesis: verum

end;

f is real-valued by A1, MESFUNC2:def 4;
hence f | A is_simple_func_in S by A32, A33, MESFUNC2:def 4; :: thesis: verum