let X be non empty set ; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let S be SigmaField of X; :: thesis:
let A be Element of S; :: thesis:
assume A1: f is_simple_func_in S ; :: thesis:
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:
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 A6: dom (f | (union (rng G))) = (dom f) /\ {} by RELAT_1:60, 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:
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:

end;

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

end;

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

proof

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

now

per cases ;

suppose A11: F . (m + 1) = {} ; :: thesis:

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:

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:

end;

suppose A12: F . (m + 1) <> {} ; :: thesis:

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 A18: |.(f . x).| < +infty by A17, Def1;
then - +infty < f . x by EXTREAL2:58;
then A19: -infty < f . x by XXREAL_3:def 3;
f . x < +infty by A18, EXTREAL2:58;
then reconsider r1 = f . x as Real by A19, XXREAL_0:14;

now

per cases ;

suppose A20: r <= r1 ; :: thesis:

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:
assume A21: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) ; :: thesis:
then A22: 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 A23: ( 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 A21;
A24: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A21, MESFUNC1:def 12;
A25: (f | (union (rng (F | (Seg (m + 1)))))) . x1 = f . x1 by A22, FUNCT_1:70;
set m1 = m + 1;
not x1 in dom (f | F1)

proof

assume x1 in dom (f | F1) ; :: thesis:
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, A20, A24, A25; :: thesis:

end;

end;

proof

end;

end;

suppose A35: r1 < r ; :: thesis:

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:
assume A36: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) ; :: thesis:
then A37: 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 A38: x1 in ((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) by A16, XBOOLE_1:23;

now

per cases by A38, XBOOLE_0:def 3;

suppose A39: x1 in (dom f) /\ (union (rng G1)) ; :: thesis:

then reconsider x1 = x1 as Element of X ;
A40: x1 in dom (f | (union (rng G1))) by A39, RELAT_1:90;
then A41: (f | (union (rng G1))) . x1 = f . x1 by FUNCT_1:70;
A42: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A36, MESFUNC1:def 12;
(f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A37, A41, FUNCT_1:70;
then x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) by A40, A42, 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:

end;

suppose x1 in (dom f) /\ (F . (m + 1)) ; :: thesis:

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:

end;

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

end;

proof

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

now

per cases by A44, XBOOLE_0:def 3;

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

end;

suppose A52: x1 in F . (m + 1) ; :: thesis:

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

end;

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

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;
then 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 A43, XBOOLE_0:def 10;
then A57: 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;
( A /\ (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) in S & A /\ (F . (m + 1)) in S ) by A8, A9, A10, A14, FINSUB_1:def 2, MESFUNC1:def 17, XXREAL_0:2;
hence A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S by A57, FINSUB_1:def 1; :: thesis:

end;

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

end;

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

end;

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

end;

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

end;

A58: 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, A58;
hence f is_measurable_on A by RELAT_1:97; :: thesis: