let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for S being SigmaField of X
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let f be PartFunc of X,ExtREAL ; :: thesis: for S being SigmaField of X
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let S be SigmaField of X; :: thesis: for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
let A be Element of S; :: thesis: ( f is_simple_func_in S implies f is_measurable_on A )
assume A1: f is_simple_func_in S ; :: thesis: f is_measurable_on A
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 A1, Def5;
reconsider F = F as FinSequence of S ;
defpred S₁[ Nat] means ( $1 <= len F implies f | (union (rng (F | (Seg $1)))) is_measurable_on A );
A4: S₁[ 0 ]

proof

assume A5: 0 <= len F ; :: thesis: f | (union (rng (F | (Seg 0 )))) is_measurable_on A
reconsider z = 0 as Nat ;
reconsider G = F | (Seg z) as FinSequence of S by FINSEQ_1:23;
A6: len G = 0 by A5, FINSEQ_1:21;
A7: G = {} by A6;
A8: dom (f | (union (rng G))) = (dom f) /\ {} by A7, RELAT_1:60, RELAT_1:90, ZFMISC_1:2
.= {} ;
A9: for r being real number holds A /\ (less_dom (f | (union (rng G))),(R_EAL r)) in S

proof

let r be real number ; :: thesis: A /\ (less_dom (f | (union (rng G))),(R_EAL r)) in S
A10: for x1 being set st x1 in less_dom (f | (union (rng G))),(R_EAL r) holds
x1 in dom (f | (union (rng G))) by MESFUNC1:def 12;
A11: less_dom (f | (union (rng G))),(R_EAL r) c= dom (f | (union (rng G))) by A10, TARSKI:def 3;
A12: less_dom (f | (union (rng G))),(R_EAL r) = {} by A8, A11, XBOOLE_1:3;
thus A /\ (less_dom (f | (union (rng G))),(R_EAL r)) in S by A12, PROB_1:10; :: thesis: verum

end;

thus f | (union (rng (F | (Seg 0 )))) is_measurable_on A by A9, MESFUNC1:def 17; :: thesis: verum

end;

A13: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A14: ( m <= len F implies f | (union (rng (F | (Seg m)))) is_measurable_on A ) ; :: thesis: S₁[m + 1]
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A15: ( m + 1 <= len F implies f | (union (rng (F | (Seg (m + 1))))) is_measurable_on A )

proof

assume A16: m + 1 <= len F ; :: thesis: f | (union (rng (F | (Seg (m + 1))))) is_measurable_on A
A17: m <= m + 1 by NAT_1:11;
A18: for r being real number holds A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S

proof

let r be real number ; :: thesis: A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S

A19: now

per cases ( F . (m + 1) = {} or F . (m + 1) <> {} ) ;

suppose A20: F . (m + 1) = {} ; :: thesis: A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S

A21: less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) = less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)

proof

reconsider G1 = F | (Seg m) as FinSequence of S by FINSEQ_1:23;
A22: 1 <= m + 1 by NAT_1:11;
A23: m + 1 in Seg (len F) by A16, A22, FINSEQ_1:3;
A24: m + 1 in dom F by A23, FINSEQ_1:def 3;
A25: F | (Seg (m + 1)) = G1 ^ <*{} *> by A20, A24, FINSEQ_5:11;
A26: rng (F | (Seg (m + 1))) = (rng G1) \/ (rng <*{} *>) by A25, FINSEQ_1:44
.= (rng G1) \/ {{} } by FINSEQ_1:56 ;
A27: union (rng (F | (Seg (m + 1)))) = (union (rng G1)) \/ (union {{} }) by A26, ZFMISC_1:96
.= (union (rng G1)) \/ {} by ZFMISC_1:31
.= union (rng G1) ;
thus less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) = less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A27; :: thesis: verum

end;

thus A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S by A14, A16, A17, A21, MESFUNC1:def 17, XXREAL_0:2; :: thesis: verum

end;

suppose A28: F . (m + 1) <> {} ; :: thesis: A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S

reconsider G1 = F | (Seg m) as FinSequence of S by FINSEQ_1:23;
A29: 1 <= m + 1 by NAT_1:11;
A30: m + 1 in Seg (len F) by A16, A29, FINSEQ_1:3;
A31: m + 1 in dom F by A30, FINSEQ_1:def 3;
A32: F . (m + 1) in rng F by A31, FUNCT_1:def 5;
A33: F . (m + 1) in S by A32;
reconsider F1 = F . (m + 1) as Subset of X by A33;
consider x being Element of X such that
A34: x in F1 by A28, SUBSET_1:10;
A35: F | (Seg (m + 1)) = G1 ^ <*(F . (m + 1))*> by A31, FINSEQ_5:11;
A36: rng (F | (Seg (m + 1))) = (rng G1) \/ (rng <*(F . (m + 1))*>) by A35, FINSEQ_1:44
.= (rng G1) \/ {(F . (m + 1))} by FINSEQ_1:56 ;
A37: union (rng (F | (Seg (m + 1)))) = (union (rng G1)) \/ (union {(F . (m + 1))}) by A36, ZFMISC_1:96
.= (union (rng G1)) \/ (F . (m + 1)) by ZFMISC_1:31 ;
A38: x in dom f by A2, A32, A34, TARSKI:def 4;
A39: f is real-valued by A1, Def5;
A40: |.(f . x).| < +infty by A38, A39, Def1;
A41: - +infty < f . x by A40, EXTREAL2:58;
A42: -infty < f . x by A41, XXREAL_3:def 3;
A43: f . x < +infty by A40, EXTREAL2:58;
reconsider r1 = f . x as Real by A42, A43, XXREAL_0:14;

A44: now

per cases ( r <= r1 or r1 < r ) ;

suppose A45: r <= r1 ; :: thesis: A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S

A46: for x1 being set st x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) holds
x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)

proof

let x1 be set ; :: thesis: ( x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) implies x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) )
assume A47: x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) ; :: thesis: x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)
A48: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by A47, MESFUNC1:def 12;
A49: x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A48, RELAT_1:90;
A50: x1 in ((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) by A37, A49, XBOOLE_1:23;
A51: ( x1 in (dom f) /\ (union (rng G1)) or x1 in (dom f) /\ (F . (m + 1)) ) by A50, XBOOLE_0:def 3;
reconsider x1 = x1 as Element of X by A47;
A52: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A47, MESFUNC1:def 12;
A53: (f | (union (rng (F | (Seg (m + 1)))))) . x1 = f . x1 by A48, FUNCT_1:70;
set m1 = m + 1;
A54: not x1 in dom (f | F1)

proof

assume A55: x1 in dom (f | F1) ; :: thesis: contradiction
A56: x1 in (dom f) /\ F1 by A55, RELAT_1:90;
A57: x1 in F . (m + 1) by A56, XBOOLE_0:def 4;
thus contradiction by A3, A31, A34, A45, A52, A53, A57; :: thesis: verum

end;

A58: x1 in dom (f | (union (rng G1))) by A51, A54, RELAT_1:90;
A59: (f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A53, A58, FUNCT_1:70;
thus x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) by A52, A58, A59, MESFUNC1:def 12; :: thesis: verum

end;

A60: less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) c= less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) by A46, TARSKI:def 3;
A61: for x1 being set st x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) holds
x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)

proof

let x1 be set ; :: thesis: ( x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) implies x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) )
assume A62: x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) ; :: thesis: x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)
A63: x1 in dom (f | (union (rng (F | (Seg m))))) by A62, MESFUNC1:def 12;
A64: x1 in (dom f) /\ (union (rng G1)) by A63, RELAT_1:90;
A65: x1 in union (rng G1) by A64, XBOOLE_0:def 4;
A66: x1 in dom f by A64, XBOOLE_0:def 4;
A67: x1 in union (rng (F | (Seg (m + 1)))) by A37, A65, XBOOLE_0:def 3;
A68: x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A66, A67, XBOOLE_0:def 4;
A69: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by A68, RELAT_1:90;
reconsider x1 = x1 as Element of X by A62;
A70: (f | (union (rng (F | (Seg m))))) . x1 < R_EAL r by A62, MESFUNC1:def 12;
A71: (f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A63, FUNCT_1:70;
A72: (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A69, A71, FUNCT_1:70;
thus x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A69, A70, A72, MESFUNC1:def 12; :: thesis: verum

end;

A73: less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) c= less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A61, TARSKI:def 3;
A74: less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) = less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) by A60, A73, XBOOLE_0:def 10;
thus A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S by A14, A16, A17, A74, MESFUNC1:def 17, XXREAL_0:2; :: thesis: verum

end;

suppose A75: r1 < r ; :: thesis: A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S

A76: for x1 being set st x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) holds
x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1))

proof

let x1 be set ; :: thesis: ( x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) implies x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) )
assume A77: x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) ; :: thesis: x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1))
A78: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by A77, MESFUNC1:def 12;
A79: x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A78, RELAT_1:90;
A80: x1 in ((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) by A37, A79, XBOOLE_1:23;

A81: now

per cases ( x1 in (dom f) /\ (union (rng G1)) or x1 in (dom f) /\ (F . (m + 1)) ) by A80, XBOOLE_0:def 3;

suppose A82: x1 in (dom f) /\ (union (rng G1)) ; :: thesis: x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1))

reconsider x1 = x1 as Element of X by A82;
A83: x1 in dom (f | (union (rng G1))) by A82, RELAT_1:90;
A84: (f | (union (rng G1))) . x1 = f . x1 by A83, FUNCT_1:70;
A85: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A77, MESFUNC1:def 12;
A86: (f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A78, A84, FUNCT_1:70;
A87: x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) by A83, A85, A86, MESFUNC1:def 12;
thus x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) by A87, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A88: x1 in (dom f) /\ (F . (m + 1)) ; :: thesis: x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1))

A89: x1 in F . (m + 1) by A88, XBOOLE_0:def 4;
thus x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) by A89, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) by A81; :: thesis: verum

end;

A90: less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) c= (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) by A76, TARSKI:def 3;
A91: for x1 being set st x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) holds
x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)

proof

let x1 be set ; :: thesis: ( x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) implies x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) )
assume A92: x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) ; :: thesis: x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)

A93: now

per cases ( x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) or x1 in F . (m + 1) ) by A92, XBOOLE_0:def 3;

suppose A94: x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) ; :: thesis: x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)

A95: x1 in dom (f | (union (rng (F | (Seg m))))) by A94, MESFUNC1:def 12;
A96: x1 in (dom f) /\ (union (rng G1)) by A95, RELAT_1:90;
A97: x1 in union (rng G1) by A96, XBOOLE_0:def 4;
A98: x1 in dom f by A96, XBOOLE_0:def 4;
A99: x1 in union (rng (F | (Seg (m + 1)))) by A37, A97, XBOOLE_0:def 3;
A100: x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A98, A99, XBOOLE_0:def 4;
A101: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by A100, RELAT_1:90;
reconsider x1 = x1 as Element of X by A94;
A102: (f | (union (rng (F | (Seg m))))) . x1 < R_EAL r by A94, MESFUNC1:def 12;
A103: (f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A95, FUNCT_1:70;
A104: (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A101, A103, FUNCT_1:70;
thus x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A101, A102, A104, MESFUNC1:def 12; :: thesis: verum

end;

suppose A105: x1 in F . (m + 1) ; :: thesis: x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)

A106: x1 in union (rng (F | (Seg (m + 1)))) by A37, A105, XBOOLE_0:def 3;
A107: x1 in dom f by A2, A32, A105, TARSKI:def 4;
A108: x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A106, A107, XBOOLE_0:def 4;
A109: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by A108, RELAT_1:90;
reconsider x1 = x1 as Element of X by A107;
A110: f . x1 = R_EAL r1 by A3, A31, A34, A105;
reconsider y = f . x1 as R_eal ;
A111: y = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A109, FUNCT_1:70;
thus x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A75, A109, A110, A111, MESFUNC1:def 12; :: thesis: verum

end;

end;

end;

thus x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A93; :: thesis: verum

end;

A112: (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) c= less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A91, TARSKI:def 3;
A113: less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) = (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) by A90, A112, XBOOLE_0:def 10;
A114: A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) = (A /\ (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (A /\ (F . (m + 1))) by A113, XBOOLE_1:23;
A115: ( A /\ (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) in S & A /\ (F . (m + 1)) in S ) by A14, A16, A17, A32, FINSUB_1:def 2, MESFUNC1:def 17, XXREAL_0:2;
thus A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S by A114, A115, FINSUB_1:def 1; :: thesis: verum

end;

end;

end;

thus A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S by A44; :: thesis: verum

end;

end;

end;

thus A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S by A19; :: thesis: verum

end;

thus f | (union (rng (F | (Seg (m + 1))))) is_measurable_on A by A18, MESFUNC1:def 17; :: thesis: verum

end;

thus S₁[m + 1] by A15; :: thesis: verum

end;

A116: for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A13);
A117: F | (Seg (len F)) = F by FINSEQ_3:55;
A118: f | (dom f) is_measurable_on A by A2, A116, A117;
thus f is_measurable_on A by A118, RELAT_1:97; :: thesis: verum