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 5;
A4: f is real-valued by A1, MESFUNC2:def 5;
set g = f | A;
deffunc H₁( Nat) -> Element of bool X = (F . $1) /\ A;
consider G being FinSequence such that
A7: ( len G = len F & ( for n being Nat st n in dom G holds
G . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A8: dom G = Seg (len F) by A7, FINSEQ_1:def 3;
rng G c= S

proof

let P be set ; :: 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
A9: ( k in dom G & P = G . k ) by FINSEQ_2:11;
A10: k in Seg (len F) by A7, A9, FINSEQ_1:def 3;
A11: G . k = (F . k) /\ A by A7, A9;
k in dom F by A10, FINSEQ_1:def 3;
then ( F . k in rng F & rng F c= S ) by FUNCT_1:12;
hence P in S by A9, A11, FINSUB_1:def 2; :: thesis: verum

end;

then reconsider G = G as FinSequence of S by 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 A12: ( i in dom G & j in dom G & i <> j ) ; :: thesis: G . i misses G . j
then ( i in Seg (len F) & j in Seg (len F) ) by A7, FINSEQ_1:def 3;
then ( i in dom F & j in dom F ) by FINSEQ_1:def 3;
then A13: F . i misses F . j by A12, MESFUNC3:4;
( G . i = (F . i) /\ A & G . j = (F . j) /\ A ) by A7, A12;
then (G . i) /\ (G . j) = (((F . i) /\ A) /\ (F . j)) /\ A by XBOOLE_1:16
.= (((F . i) /\ (F . j)) /\ A) /\ A by XBOOLE_1:16
.= ({} /\ A) /\ A by A13, XBOOLE_0:def 7 ;
hence G . i misses G . j by XBOOLE_0:def 7; :: thesis: verum

end;

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

proof

let v be set ; :: 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 v in (dom f) /\ A by RELAT_1:90;
then A14: ( v in dom f & v in A ) by XBOOLE_0:def 4;
then consider W being set such that
A15: ( v in W & W in rng F ) by A2, TARSKI:def 4;
consider k being Nat such that
A16: ( k in dom F & W = F . k ) by A15, FINSEQ_2:11;
A17: k in Seg (len F) by A16, FINSEQ_1:def 3;
then G . k = (F . k) /\ A by A7, A8;
then A18: v in G . k by A14, A15, A16, XBOOLE_0:def 4;
k in dom G by A7, A17, FINSEQ_1:def 3;
then G . k in rng G by FUNCT_1:12;
hence v in union (rng G) by A18, TARSKI:def 4; :: thesis: verum

end;

then A19: dom (f | A) c= union (rng G) by TARSKI:def 3;
for v being set st v in union (rng G) holds
v in dom (f | A)

proof

let v be set ; :: 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
A20: ( v in W & W in rng G ) by TARSKI:def 4;
consider k being Nat such that
A21: ( k in dom G & W = G . k ) by A20, FINSEQ_2:11;
A22: k in Seg (len F) by A7, A21, FINSEQ_1:def 3;
G . k = (F . k) /\ A by A7, A21;
then A23: ( v in F . k & v in A ) by A20, A21, XBOOLE_0:def 4;
k in dom F by A22, FINSEQ_1:def 3;
then F . k in rng F by FUNCT_1:12;
then v in union (rng F) by A23, TARSKI:def 4;
then v in (dom f) /\ A by A2, A23, XBOOLE_0:def 4;
hence v in dom (f | A) by RELAT_1:90; :: thesis: verum

end;

then union (rng G) c= dom (f | A) by TARSKI:def 3;
then A24: dom (f | A) = union (rng G) by A19, XBOOLE_0:def 10;
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 A25: ( n in dom G & x in G . n & y in G . n ) ; :: thesis: (f | A) . x = (f | A) . y
then G . n in rng G by FUNCT_1:12;
then A26: ( x in dom (f | A) & y in dom (f | A) ) by A24, A25, TARSKI:def 4;
A27: n in Seg (len F) by A7, A25, FINSEQ_1:def 3;
G . n = (F . n) /\ A by A7, A25;
then A28: ( x in F . n & y in F . n ) by A25, XBOOLE_0:def 4;
n in dom F by A27, FINSEQ_1:def 3;
then f . x = f . y by A3, A28;
then (f | A) . x = f . y by A26, FUNCT_1:70;
hence (f | A) . x = (f | A) . y by A26, FUNCT_1:70; :: thesis: verum

end;

hence f | A is_simple_func_in S by A4, A24, MESFUNC2:def 5; :: thesis: verum