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 A -measurable

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 A -measurable

let S be SigmaField of X; :: thesis: for A being Element of S st f is_simple_func_in S holds

f is A -measurable

let A be Element of S; :: thesis: ( f is_simple_func_in S implies f is A -measurable )

assume A1: f is_simple_func_in S ; :: thesis: f is A -measurable

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_{1}[ Nat] means ( $1 <= len F implies f | (union (rng (F | (Seg $1)))) is A -measurable );

A4: S_{1}[ 0 ]
_{1}[m] holds

S_{1}[m + 1]
_{1}[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: verum

for S being SigmaField of X

for A being Element of S st f is_simple_func_in S holds

f is A -measurable

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 A -measurable

let S be SigmaField of X; :: thesis: for A being Element of S st f is_simple_func_in S holds

f is A -measurable

let A be Element of S; :: thesis: ( f is_simple_func_in S implies f is A -measurable )

assume A1: f is_simple_func_in S ; :: thesis: f is A -measurable

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

A4: S

proof

A7:
for m being Nat st S
assume A5:
0 <= len F
; :: thesis: f | (union (rng (F | (Seg 0)))) is A -measurable

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

end;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

hence
f | (union (rng (F | (Seg 0)))) is A -measurable
; :: thesis: verum
let r be Real; :: thesis: A /\ (less_dom ((f | (union (rng G))),r)) in S

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: verum

end;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: verum

S

proof

A58:
for n being Nat holds S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A8: ( m <= len F implies f | (union (rng (F | (Seg m)))) is A -measurable ) ; :: thesis: S_{1}[m + 1]

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 )_{1}[m + 1]
; :: thesis: verum

end;assume A8: ( m <= len F implies f | (union (rng (F | (Seg m)))) is A -measurable ) ; :: thesis: S

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

hence
S
assume A9:
m + 1 <= len F
; :: thesis: f | (union (rng (F | (Seg (m + 1))))) is A -measurable

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

end;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

hence
f | (union (rng (F | (Seg (m + 1))))) is A -measurable
; :: thesis: verum
let r be Real; :: thesis: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)) in S

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

hence
A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)) in S
; :: thesis: verumper cases
( F . (m + 1) = {} or F . (m + 1) <> {} )
;

end;

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

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

end;proof

hence
A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)) in S
by A8, A9, A10, XXREAL_0:2; :: thesis: verum
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: verum

end;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: verum

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

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 V82() 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;

end;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 V82() 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: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)) in Send;

hence
A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)) in S
; :: thesis: verumper cases
( r <= r1 or r1 < r )
;

end;

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

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)

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

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

then less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) = less_dom ((f | (union (rng (F | (Seg m))))),r) by A27;

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

end;x1 in less_dom ((f | (union (rng (F | (Seg m))))),r)

proof

then A27:
less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) c= less_dom ((f | (union (rng (F | (Seg m))))),r)
;
let x1 be object ; :: thesis: ( x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) implies x1 in less_dom ((f | (union (rng (F | (Seg m))))),r) )

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

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)

then (f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A25, FUNCT_1:47;

hence x1 in less_dom ((f | (union (rng (F | (Seg m))))),r) by A24, A26, MESFUNC1:def 11; :: thesis: verum

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

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

then A26:
x1 in dom (f | (union (rng G1)))
by A23, RELAT_1:61;
assume
x1 in dom (f | F1)
; :: thesis: contradiction

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: verum

end;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: verum

then (f | (union (rng (F | (Seg (m + 1)))))) . x1 = (f | (union (rng G1))) . x1 by A25, FUNCT_1:47;

hence x1 in less_dom ((f | (union (rng (F | (Seg m))))),r) by A24, A26, MESFUNC1:def 11; :: thesis: verum

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

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

proof

then
less_dom ((f | (union (rng (F | (Seg m))))),r) c= less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)
;
let x1 be object ; :: thesis: ( x1 in less_dom ((f | (union (rng (F | (Seg m))))),r) implies x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) )

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

then A29: x1 in dom (f | (union (rng (F | (Seg m))))) by MESFUNC1:def 11;

then A30: x1 in (dom f) /\ (union (rng G1)) by RELAT_1:61;

then A31: x1 in union (rng G1) by XBOOLE_0:def 4;

A32: x1 in dom f by A30, XBOOLE_0:def 4;

x1 in union (rng (F | (Seg (m + 1)))) by A16, A31, XBOOLE_0:def 3;

then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A32, XBOOLE_0:def 4;

then A33: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:61;

reconsider x1 = x1 as Element of X by A28;

A34: (f | (union (rng (F | (Seg m))))) . x1 < r by A28, MESFUNC1:def 11;

(f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A29, FUNCT_1:47;

then (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A33, FUNCT_1:47;

hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) by A33, A34, MESFUNC1:def 11; :: thesis: verum

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

then A29: x1 in dom (f | (union (rng (F | (Seg m))))) by MESFUNC1:def 11;

then A30: x1 in (dom f) /\ (union (rng G1)) by RELAT_1:61;

then A31: x1 in union (rng G1) by XBOOLE_0:def 4;

A32: x1 in dom f by A30, XBOOLE_0:def 4;

x1 in union (rng (F | (Seg (m + 1)))) by A16, A31, XBOOLE_0:def 3;

then x1 in (dom f) /\ (union (rng (F | (Seg (m + 1))))) by A32, XBOOLE_0:def 4;

then A33: x1 in dom (f | (union (rng (F | (Seg (m + 1)))))) by RELAT_1:61;

reconsider x1 = x1 as Element of X by A28;

A34: (f | (union (rng (F | (Seg m))))) . x1 < r by A28, MESFUNC1:def 11;

(f | (union (rng (F | (Seg m))))) . x1 = f . x1 by A29, FUNCT_1:47;

then (f | (union (rng (F | (Seg m))))) . x1 = (f | (union (rng (F | (Seg (m + 1)))))) . x1 by A33, FUNCT_1:47;

hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) by A33, A34, MESFUNC1:def 11; :: thesis: verum

then less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) = less_dom ((f | (union (rng (F | (Seg m))))),r) by A27;

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

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

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

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

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

then less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) = (less_dom ((f | (union (rng (F | (Seg m))))),r)) \/ (F . (m + 1)) by A43;

then A57: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)) = (A /\ (less_dom ((f | (union (rng (F | (Seg m))))),r))) \/ (A /\ (F . (m + 1))) by XBOOLE_1:23;

( A /\ (less_dom ((f | (union (rng (F | (Seg m))))),r)) in S & A /\ (F . (m + 1)) in S ) by A8, A9, A10, A14, FINSUB_1:def 2, XXREAL_0:2;

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

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

proof

then A43:
less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) c= (less_dom ((f | (union (rng (F | (Seg m))))),r)) \/ (F . (m + 1))
;
let x1 be object ; :: thesis: ( x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) implies x1 in (less_dom ((f | (union (rng (F | (Seg m))))),r)) \/ (F . (m + 1)) )

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

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;

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

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: x1 in (less_dom ((f | (union (rng (F | (Seg m))))),r)) \/ (F . (m + 1))end;

hence
x1 in (less_dom ((f | (union (rng (F | (Seg m))))),r)) \/ (F . (m + 1))
; :: thesis: verumper cases
( x1 in (dom f) /\ (union (rng G1)) or x1 in (dom f) /\ (F . (m + 1)) )
by A38, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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

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

proof

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

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

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

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

hence
x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)
; :: thesis: verumper cases
( x1 in less_dom ((f | (union (rng (F | (Seg m))))),r) or x1 in F . (m + 1) )
by A44, XBOOLE_0:def 3;

end;

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

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: verum

end;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: verum

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

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: verum

end;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: verum

then less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r) = (less_dom ((f | (union (rng (F | (Seg m))))),r)) \/ (F . (m + 1)) by A43;

then A57: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),r)) = (A /\ (less_dom ((f | (union (rng (F | (Seg m))))),r))) \/ (A /\ (F . (m + 1))) by XBOOLE_1:23;

( A /\ (less_dom ((f | (union (rng (F | (Seg m))))),r)) in S & A /\ (F . (m + 1)) in S ) by A8, A9, A10, A14, FINSUB_1:def 2, XXREAL_0:2;

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

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: verum