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_{1}( 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_{1}(n) ) )
from FINSEQ_1:sch 2();

A5: rng G c= S

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

for v being object st v in union (rng G) holds

v in dom (f | A)

for v being object st v in dom (f | A) holds

v in 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

hence f | A is_simple_func_in S by A32, A33, MESFUNC2:def 4; :: thesis: verum

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

consider G being FinSequence such that

A4: ( len G = len F & ( for n being Nat st n in dom G holds

G . n = H

A5: rng G c= S

proof

A9:
dom G = Seg (len F)
by A4, FINSEQ_1:def 3;
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;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

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

then reconsider G = G as Finite_Sep_Sequence of S by MESFUNC3:4;
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;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

for v being object st v in union (rng G) holds

v in dom (f | A)

proof

then A23:
union (rng G) c= dom (f | A)
;
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;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

for v being object st v in dom (f | A) holds

v in union (rng G)

proof

then
dom (f | A) c= union (rng G)
;
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;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

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

f is real-valued
by A1, MESFUNC2:def 4;
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 | 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

hence f | A is_simple_func_in S by A32, A33, MESFUNC2:def 4; :: thesis: verum