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 A8: 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 A8, 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;

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

proof

let m be Nat; :: thesis:
assume A14: ( 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 A16: m + 1 <= len F ; :: thesis:
A17: 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 A20: 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 A16, FINSEQ_1:3;
then m + 1 in dom F by FINSEQ_1:def 3;
then F | (Seg (m + 1)) = G1 ^ <*{}*> by A20, 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 A14, A16, A17, MESFUNC1:def 17, XXREAL_0:2; :: thesis:

end;

suppose A28: 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 A16, FINSEQ_1:3;
then A31: m + 1 in dom F by FINSEQ_1:def 3;
then A32: 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
A34: x in F1 by A28, SUBSET_1:10;
F | (Seg (m + 1)) = G1 ^ <*(F . (m + 1))*> by A31, 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 A37: 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 ;
A38: x in dom f by A2, A32, A34, TARSKI:def 4;
f is real-valued by A1, Def5;
then A40: |.(f . x).| < +infty by A38, Def1;
then - +infty < f . x by EXTREAL2:58;
then A42: -infty < f . x by XXREAL_3:def 3;
f . x < +infty by A40, EXTREAL2:58;
then reconsider r1 = f . x as Real by A42, XXREAL_0:14;

now

per cases ;

suppose A45: 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 A47: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) ; :: thesis:
then A48: 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 A37, XBOOLE_1:23;
then A51: ( 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 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;
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, A31, A34, A45, A52, A53; :: thesis:

end;

end;

proof

end;

end;

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

now

per cases by A80, XBOOLE_0:def 3;

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

then reconsider x1 = x1 as Element of X ;
A83: x1 in dom (f | (union (rng G1))) by A82, RELAT_1:90;
then A84: (f | (union (rng G1))) . x1 = f . x1 by FUNCT_1:70;
A85: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < R_EAL r by A77, MESFUNC1:def 12;
(f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A78, A84, FUNCT_1:70;
then x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) by A83, A85, 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 A92: x1 in (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) ; :: thesis:

now

per cases by A92, XBOOLE_0:def 3;

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

then A95: x1 in dom (f | (union (rng (F | (Seg m))))) by MESFUNC1:def 12;
then A96: x1 in (dom f) /\ (union (rng G1)) by RELAT_1:90;
then A97: x1 in union (rng G1) by XBOOLE_0:def 4;
A98: x1 in dom f by A96, XBOOLE_0:def 4;
x1 in union (rng (F | (Seg (m + 1)))) by A37, A97, XBOOLE_0:def 3;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A98, XBOOLE_0:def 4;
then A101: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by 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;
(f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A95, FUNCT_1:70;
then (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A101, FUNCT_1:70;
hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) by A101, A102, MESFUNC1:def 12; :: thesis:

end;

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

then A106: x1 in union (rng (F | (Seg (m + 1)))) by A37, XBOOLE_0:def 3;
A107: x1 in dom f by A2, A32, A105, TARSKI:def 4;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A106, XBOOLE_0:def 4;
then A109: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by 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 ;
y = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A109, FUNCT_1:70;
hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) by A75, A109, A110, MESFUNC1:def 12; :: thesis:

end;

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

end;

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;

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