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 ;
reconsider F = F as FinSequence of S ;
defpred S₁[ Nat] means ( $1 <= len F implies f | (union (rng (F | (Seg $1)))) is A -measurable );
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:18;
len G = 0 by A5, FINSEQ_1:17;
then G = {} ;
then A6: dom (f | (union (rng G))) = (dom f) /\ {} by RELAT_1:38, RELAT_1:61, ZFMISC_1:2
.= {} ;
for r being Real holds A /\ (less_dom ((f | (union (rng G))),r)) in S

proof

let r be Real; :: thesis:
for x1 being object st x1 in less_dom ((f | (union (rng G))),r) holds
x1 in dom (f | (union (rng G))) by MESFUNC1:def 11;
then less_dom ((f | (union (rng G))),r) c= dom (f | (union (rng G))) ;
then less_dom ((f | (union (rng G))),r) = {} by A6, XBOOLE_1:3;
hence A /\ (less_dom ((f | (union (rng G))),r)) in S by PROB_1:4; :: thesis:

end;

hence f | (union (rng (F | (Seg 0)))) is A -measurable ; :: 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 A -measurable ) ; :: thesis:
reconsider m = m as Element of NAT by ORDINAL1:def 12;
( m + 1 <= len F implies f | (union (rng (F | (Seg (m + 1))))) is A -measurable )

proof

assume A9: m + 1 <= len F ; :: thesis:
A10: m <= m + 1 by NAT_1:11;
for r being Real holds A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)) in S

proof

let r be Real; :: thesis:

now :: thesis:

per cases ;

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

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

proof

reconsider G1 = F | (Seg m) as FinSequence of S by FINSEQ_1:18;
1 <= m + 1 by NAT_1:11;
then m + 1 in Seg (len F) by A9, FINSEQ_1:1;
then m + 1 in dom F by FINSEQ_1:def 3;
then F | (Seg (m + 1)) = G1 ^ <*{}*> by A11, FINSEQ_5:10;
then rng (F | (Seg (m + 1))) = (rng G1) \/ (rng <*{}*>) by FINSEQ_1:31
.= (rng G1) \/ {{}} by FINSEQ_1:39 ;
then union (rng (F | (Seg (m + 1)))) = (union (rng G1)) \/ (union {{}}) by ZFMISC_1:78
.= (union (rng G1)) \/ {} by ZFMISC_1:25
.= union (rng G1) ;
hence less_dom ((f | (union (rng (F | (Seg m))))),r) = less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) ; :: thesis:

end;

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

end;

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

reconsider G1 = F | (Seg m) as FinSequence of S by FINSEQ_1:18;
1 <= m + 1 by NAT_1:11;
then m + 1 in Seg (len F) by A9, FINSEQ_1:1;
then A13: m + 1 in dom F by FINSEQ_1:def 3;
then A14: F . (m + 1) in rng F by FUNCT_1:def 3;
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:4;
F | (Seg (m + 1)) = G1 ^ <*(F . (m + 1))*> by A13, FINSEQ_5:10;
then rng (F | (Seg (m + 1))) = (rng G1) \/ (rng <*(F . (m + 1))*>) by FINSEQ_1:31
.= (rng G1) \/ {(F . (m + 1))} by FINSEQ_1:39 ;
then A16: union (rng (F | (Seg (m + 1)))) = (union (rng G1)) \/ (union {(F . (m + 1))}) by ZFMISC_1:78
.= (union (rng G1)) \/ (F . (m + 1)) by ZFMISC_1:25 ;
A17: x in dom f by A2, A14, A15, TARSKI:def 4;
f is real-valued by A1;
then A18: |.(f . x).| < +infty by A17;
then - +infty < f . x by EXTREAL1:21;
then A19: -infty < f . x by XXREAL_3:def 3;
f . x < +infty by A18, EXTREAL1:21;
then reconsider r1 = f . x as Element of REAL by A19, XXREAL_0:14;

now :: thesis:

per cases ;

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

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

proof

let x1 be object ; :: thesis:
assume A21: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) ; :: thesis:
then A22: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by MESFUNC1:def 11;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by RELAT_1:61;
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 by A21, MESFUNC1:def 11;
A25: (f | (union (rng (F | (Seg (m + 1)))))) . x1 = f . x1 by A22, FUNCT_1:47;
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:61;
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 object st x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) holds
x1 in (less_dom ((f | (union (rng (F | (Seg m))))),r)) \/ (F . (m + 1))

proof

let x1 be object ; :: thesis:
assume A36: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) ; :: thesis:
then A37: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by MESFUNC1:def 11;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by RELAT_1:61;
then A38: x1 in ((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) by A16, XBOOLE_1:23;

now :: thesis:

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:61;
then A41: (f | (union (rng G1))) . x1 = f . x1 by FUNCT_1:47;
A42: (f | (union (rng (F | (Seg (m + 1)))))) . x1 < r by A36, MESFUNC1:def 11;
(f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A37, A41, FUNCT_1:47;
then x1 in less_dom ((f | (union (rng (F | (Seg m))))),r) by A40, A42, MESFUNC1:def 11;
hence x1 in (less_dom ((f | (union (rng (F | (Seg m))))),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)) \/ (F . (m + 1)) by XBOOLE_0:def 3; :: thesis:

end;

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

end;

proof

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

now :: thesis:

per cases by A44, XBOOLE_0:def 3;

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

then A46: x1 in dom (f | (union (rng (F | (Seg m))))) by MESFUNC1:def 11;
then A47: x1 in (dom f) /\ (union (rng G1)) by RELAT_1:61;
then A48: x1 in union (rng G1) by XBOOLE_0:def 4;
A49: x1 in dom f by A47, XBOOLE_0:def 4;
x1 in union (rng (F | (Seg (m + 1)))) by A16, A48, XBOOLE_0:def 3;
then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A49, XBOOLE_0:def 4;
then A50: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:61;
reconsider x1 = x1 as Element of X by A45;
A51: (f | (union (rng (F | (Seg m))))) . x1 < r by A45, MESFUNC1:def 11;
(f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A46, FUNCT_1:47;
then (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A50, FUNCT_1:47;
hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) by A50, A51, MESFUNC1:def 11; :: 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:61;
reconsider x1 = x1 as Element of X by A54;
A56: f . x1 = 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:47;
hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) by A35, A55, A56, MESFUNC1:def 11; :: thesis:

end;

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

end;

end;

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

end;

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

end;

hence f | (union (rng (F | (Seg (m + 1))))) is A -measurable ; :: 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:49;
then f | (dom f) is A -measurable by A2, A58;
hence f is A -measurable by RELAT_1:68; :: thesis: