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
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 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;
len G = 0 by A5, FINSEQ_1:21;
then G = {} ;
then rng G = {} by RELAT_1:60;
then A6: dom (f | (union (rng G))) = (dom f) /\ {} by RELAT_1:90, ZFMISC_1:2
.= {} ;
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
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;
then less_dom (f | (union (rng G))),(R_EAL r) c= dom (f | (union (rng G))) by TARSKI:def 3;
then less_dom (f | (union (rng G))),(R_EAL r) = {} by A6, XBOOLE_1:3;
hence A /\ (less_dom (f | (union (rng G))),(R_EAL r)) in S by PROB_1:10; :: thesis: verum

end;

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

end;

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

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A8: ( 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;
( m + 1 <= len F implies f | (union (rng (F | (Seg (m + 1))))) is_measurable_on A )

proof

assume A9: m + 1 <= len F ; :: thesis: f | (union (rng (F | (Seg (m + 1))))) is_measurable_on A
A10: m <= m + 1 by NAT_1:11;
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

now

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

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

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;
1 <= m + 1 by NAT_1:11;
then m + 1 in Seg (len F) by A9, FINSEQ_1:3;
then m + 1 in dom F by FINSEQ_1:def 3;
then F | (Seg (m + 1)) = G1 ^ <*{} *> by A11, FINSEQ_5:11;
then rng (F | (Seg (m + 1))) = (rng G1) \/ (rng <*{} *>) by FINSEQ_1:44
.= (rng G1) \/ {{} } by FINSEQ_1:56 ;
then union (rng (F | (Seg (m + 1)))) = (union (rng G1)) \/ (union {{} }) by ZFMISC_1:96
.= (union (rng G1)) \/ {} by ZFMISC_1:31
.= union (rng G1) ;
hence less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) = less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) ; :: thesis: verum

end;

hence A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S by A8, A9, A10, MESFUNC1:def 17, XXREAL_0:2; :: thesis: verum

end;

suppose A12: 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;
1 <= m + 1 by NAT_1:11;
then m + 1 in Seg (len F) by A9, FINSEQ_1:3;
then A13: m + 1 in dom F by FINSEQ_1:def 3;
then A14: F . (m + 1) in rng F by FUNCT_1:def 5;
then F . (m + 1) in S ;
then reconsider F1 = F . (m + 1) as Subset of X ;
consider x being Element of X such that
A15: x in F1 by A12, SUBSET_1:10;
F | (Seg (m + 1)) = G1 ^ <*(F . (m + 1))*> by A13, FINSEQ_5:11;
then rng (F | (Seg (m + 1))) = (rng G1) \/ (rng <*(F . (m + 1))*>) by FINSEQ_1:44
.= (rng G1) \/ {(F . (m + 1))} by FINSEQ_1:56 ;
then A16: union (rng (F | (Seg (m + 1)))) = (union (rng G1)) \/ (union {(F . (m + 1))}) by ZFMISC_1:96
.= (union (rng G1)) \/ (F . (m + 1)) by ZFMISC_1:31 ;
A17: x in dom f by A2, A14, A15, TARSKI:def 4;
f is real-valued by A1, Def5;
then |.(f . x).| < +infty by A17, Def1;
then ( - +infty < f . x & f . x < +infty ) by EXTREAL2:58;
then ( -infty < f . x & f . x < +infty ) by XXREAL_3:def 3;
then reconsider r1 = f . x as Real by XXREAL_0:14;

now

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

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

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

proof

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 A19: 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)
then A20: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by MESFUNC1:def 12;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by RELAT_1:90;
then x1 in ((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) by A16, XBOOLE_1:23;
then A21: ( x1 in (dom f) /\ (union (rng G1)) or x1 in (dom f) /\ (F . (m + 1)) ) by XBOOLE_0:def 3;
reconsider x1 = x1 as Element of X by A19;
A22: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A19, MESFUNC1:def 12;
A23: (f | (union (rng (F | (Seg (m + 1)))))) . x1 = f . x1 by A20, FUNCT_1:70;
set m1 = m + 1;
not x1 in dom (f | F1)

proof

assume x1 in dom (f | F1) ; :: thesis: contradiction
then x1 in (dom f) /\ F1 by RELAT_1:90;
then x1 in F . (m + 1) by XBOOLE_0:def 4;
hence contradiction by A3, A13, A15, A18, A22, A23; :: thesis: verum

end;

then A24: x1 in dom (f | (union (rng G1))) by A21, RELAT_1:90;
then (f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A23, FUNCT_1:70;
hence x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) by A22, A24, MESFUNC1:def 12; :: thesis: verum

end;

then A25: 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 TARSKI:def 3;
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 A26: 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)
then A27: x1 in dom (f | (union (rng (F | (Seg m))))) by MESFUNC1:def 12;
then x1 in (dom f) /\ (union (rng G1)) by RELAT_1:90;
then ( x1 in dom f & x1 in union (rng G1) ) by XBOOLE_0:def 4;
then ( x1 in dom f & x1 in union (rng (F | (Seg (m + 1)))) ) by A16, XBOOLE_0:def 3;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by XBOOLE_0:def 4;
then A28: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:90;
reconsider x1 = x1 as Element of X by A26;
A29: (f | (union (rng (F | (Seg m))))) . x1 < R_EAL r by A26, MESFUNC1:def 12;
(f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A27, FUNCT_1:70;
then (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A28, FUNCT_1:70;
hence x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A28, A29, MESFUNC1:def 12; :: thesis: verum

end;

then 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 TARSKI:def 3;
hence less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) = less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) by A25, XBOOLE_0:def 10; :: thesis: verum

end;

hence A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S by A8, A9, A10, MESFUNC1:def 17, XXREAL_0:2; :: thesis: verum

end;

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

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))

proof

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 A31: 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))
then A32: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by MESFUNC1:def 12;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by RELAT_1:90;
then A33: x1 in ((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) by A16, XBOOLE_1:23;

now

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

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

then reconsider x1 = x1 as Element of X ;
A35: x1 in dom (f | (union (rng G1))) by A34, RELAT_1:90;
then A36: (f | (union (rng G1))) . x1 = f . x1 by FUNCT_1:70;
A37: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A31, MESFUNC1:def 12;
(f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A32, A36, FUNCT_1:70;
then x1 in less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r) by A35, A37, MESFUNC1:def 12;
hence x1 in (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) \/ (F . (m + 1)) by XBOOLE_0:def 3; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

then A38: 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 TARSKI:def 3;
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 A39: 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)

now

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

suppose A40: 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)

then A41: x1 in dom (f | (union (rng (F | (Seg m))))) by MESFUNC1:def 12;
then x1 in (dom f) /\ (union (rng G1)) by RELAT_1:90;
then ( x1 in dom f & x1 in union (rng G1) ) by XBOOLE_0:def 4;
then ( x1 in dom f & x1 in union (rng (F | (Seg (m + 1)))) ) by A16, XBOOLE_0:def 3;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by XBOOLE_0:def 4;
then A42: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:90;
reconsider x1 = x1 as Element of X by A40;
A43: (f | (union (rng (F | (Seg m))))) . x1 < R_EAL r by A40, MESFUNC1:def 12;
(f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A41, FUNCT_1:70;
then (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A42, FUNCT_1:70;
hence x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A42, A43, MESFUNC1:def 12; :: thesis: verum

end;

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

then A45: x1 in union (rng (F | (Seg (m + 1)))) by A16, XBOOLE_0:def 3;
A46: x1 in dom f by A2, A14, A44, TARSKI:def 4;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A45, XBOOLE_0:def 4;
then A47: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:90;
reconsider x1 = x1 as Element of X by A46;
A48: f . x1 = R_EAL r1 by A3, A13, A15, A44;
reconsider y = f . x1 as R_eal ;
y = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A47, FUNCT_1:70;
hence x1 in less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r) by A30, A47, A48, MESFUNC1:def 12; :: thesis: verum

end;

end;

end;

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

end;

then (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 TARSKI:def 3;
hence 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 A38, XBOOLE_0:def 10; :: thesis: verum

end;

then A49: 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 XBOOLE_1:23;
A50: A /\ (less_dom (f | (union (rng (F | (Seg m))))),(R_EAL r)) in S by A8, A9, A10, MESFUNC1:def 17, XXREAL_0:2;
A /\ (F . (m + 1)) in S by A14, MEASURE1:19;
hence A /\ (less_dom (f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) in S by A49, A50, FINSUB_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

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

end;

hence S₁[m + 1] ; :: thesis: verum

end;

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