:: MESFUNC2 semantic presentation begin definition let X be non empty set ; let f be PartFunc of X,ExtREAL; :: original: real-valued redefine attrf is real-valued means :Def1: :: MESFUNC2:def 1 for x being Element of X st x in dom f holds |.(f . x).| < +infty ; compatibility ( f is real-valued iff for x being Element of X st x in dom f holds |.(f . x).| < +infty ) proof thus ( f is real-valued implies for x being Element of X st x in dom f holds |.(f . x).| < +infty ) ::_thesis: ( ( for x being Element of X st x in dom f holds |.(f . x).| < +infty ) implies f is real-valued ) proof assume A1: f is real-valued ; ::_thesis: for x being Element of X st x in dom f holds |.(f . x).| < +infty let x be Element of X; ::_thesis: ( x in dom f implies |.(f . x).| < +infty ) assume x in dom f ; ::_thesis: |.(f . x).| < +infty then A2: f . x in rng f by FUNCT_1:3; rng f c= REAL by A1, VALUED_0:def_3; hence |.(f . x).| < +infty by A2, EXTREAL2:30; ::_thesis: verum end; assume A3: for x being Element of X st x in dom f holds |.(f . x).| < +infty ; ::_thesis: f is real-valued let e be set ; :: according to VALUED_0:def_9 ::_thesis: ( not e in dom f or f . e is real ) assume A4: e in dom f ; ::_thesis: f . e is real then reconsider x = e as Element of X ; |.(f . x).| < +infty by A3, A4; then f . x in REAL by EXTREAL2:30; hence f . e is real ; ::_thesis: verum end; end; :: deftheorem Def1 defines real-valued MESFUNC2:def_1_:_ for X being non empty set for f being PartFunc of X,ExtREAL holds ( f is real-valued iff for x being Element of X st x in dom f holds |.(f . x).| < +infty ); theorem :: MESFUNC2:1 for X being non empty set for f being PartFunc of X,ExtREAL holds f = 1 (#) f proof let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL holds f = 1 (#) f let f be PartFunc of X,ExtREAL; ::_thesis: f = 1 (#) f A1: dom f = dom (1 (#) f) by MESFUNC1:def_6; for x being Element of X st x in dom (1 (#) f) holds f . x = (1 (#) f) . x proof let x be Element of X; ::_thesis: ( x in dom (1 (#) f) implies f . x = (1 (#) f) . x ) assume x in dom (1 (#) f) ; ::_thesis: f . x = (1 (#) f) . x then (1 (#) f) . x = (R_EAL 1) * (f . x) by MESFUNC1:def_6; hence f . x = (1 (#) f) . x by XXREAL_3:81; ::_thesis: verum end; hence f = 1 (#) f by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th2: :: MESFUNC2:2 for X being non empty set for f, g being PartFunc of X,ExtREAL st ( not f is V75() or not g is V75() ) holds ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL st ( not f is V75() or not g is V75() ) holds ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) let f, g be PartFunc of X,ExtREAL; ::_thesis: ( ( not f is V75() or not g is V75() ) implies ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) ) assume A1: ( not f is V75() or not g is V75() ) ; ::_thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) now__::_thesis:_(_dom_(f_+_g)_=_(dom_f)_/\_(dom_g)_&_dom_(f_-_g)_=_(dom_f)_/\_(dom_g)_) percases ( not f is V75() or not g is V75() ) by A1; supposeA2: f is V75() ; ::_thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) then not +infty in rng f ; then A3: f " {+infty} = {} by FUNCT_1:72; not -infty in rng f by A2; then A4: f " {-infty} = {} by FUNCT_1:72; then A5: ((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty})) = {} by A3; A6: ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A3, A4; dom (f + g) = ((dom f) /\ (dom g)) \ {} by A5, MESFUNC1:def_3; hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A6, MESFUNC1:def_4; ::_thesis: verum end; supposeA7: g is V75() ; ::_thesis: ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) then not +infty in rng g ; then A8: g " {+infty} = {} by FUNCT_1:72; not -infty in rng g by A7; then A9: g " {-infty} = {} by FUNCT_1:72; then A10: ((f " {+infty}) /\ (g " {-infty})) \/ ((f " {-infty}) /\ (g " {+infty})) = {} by A8; A11: ((f " {+infty}) /\ (g " {+infty})) \/ ((f " {-infty}) /\ (g " {-infty})) = {} by A8, A9; dom (f + g) = ((dom f) /\ (dom g)) \ {} by A10, MESFUNC1:def_3; hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) by A11, MESFUNC1:def_4; ::_thesis: verum end; end; end; hence ( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) ) ; ::_thesis: verum end; theorem Th3: :: MESFUNC2:3 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for F being Function of RAT,S for r being Real for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for F being Function of RAT,S for r being Real for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL for F being Function of RAT,S for r being Real for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) let f, g be PartFunc of X,ExtREAL; ::_thesis: for F being Function of RAT,S for r being Real for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) let F be Function of RAT,S; ::_thesis: for r being Real for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) let r be Real; ::_thesis: for A being Element of S st f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) let A be Element of S; ::_thesis: ( f is V75() & g is V75() & ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) implies A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) ) assume that A1: f is V75() and A2: g is V75() and A3: for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ; ::_thesis: A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) A4: dom (f + g) = (dom f) /\ (dom g) by A1, Th2; A5: A /\ (less_dom ((f + g),(R_EAL r))) c= union (rng F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ (less_dom ((f + g),(R_EAL r))) or x in union (rng F) ) assume A6: x in A /\ (less_dom ((f + g),(R_EAL r))) ; ::_thesis: x in union (rng F) then A7: x in A by XBOOLE_0:def_4; A8: x in less_dom ((f + g),(R_EAL r)) by A6, XBOOLE_0:def_4; then A9: x in dom (f + g) by MESFUNC1:def_11; A10: (f + g) . x < R_EAL r by A8, MESFUNC1:def_11; reconsider x = x as Element of X by A6; A11: (f . x) + (g . x) < R_EAL r by A9, A10, MESFUNC1:def_3; A12: x in dom f by A4, A9, XBOOLE_0:def_4; A13: x in dom g by A4, A9, XBOOLE_0:def_4; A14: |.(f . x).| < +infty by A1, A12, Def1; A15: |.(g . x).| < +infty by A2, A13, Def1; A16: - +infty < f . x by A14, EXTREAL2:10; A17: f . x < +infty by A14, EXTREAL2:10; A18: - +infty < g . x by A15, EXTREAL2:10; A19: g . x < +infty by A15, EXTREAL2:10; then A20: f . x < (R_EAL r) - (g . x) by A11, A17, XXREAL_3:52; A21: -infty < f . x by A16, XXREAL_3:23; A22: -infty < g . x by A18, XXREAL_3:23; reconsider f1 = f . x as Real by A17, A21, XXREAL_0:14; reconsider g1 = g . x as Real by A19, A22, XXREAL_0:14; (R_EAL r) - (g . x) = r - g1 by SUPINF_2:3; then consider p being Rational such that A23: f1 < p and A24: p < r - g1 by A20, RAT_1:7; A25: not r - p <= g1 by A24, XREAL_1:12; A26: x in less_dom (f,(R_EAL p)) by A12, A23, MESFUNC1:def_11; A27: x in less_dom (g,(R_EAL (r - p))) by A13, A25, MESFUNC1:def_11; A28: x in A /\ (less_dom (f,(R_EAL p))) by A7, A26, XBOOLE_0:def_4; x in A /\ (less_dom (g,(R_EAL (r - p)))) by A7, A27, XBOOLE_0:def_4; then A29: x in (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A28, XBOOLE_0:def_4; p in RAT by RAT_1:def_2; then A30: p in dom F by FUNCT_2:def_1; A31: x in F . p by A3, A29; F . p in rng F by A30, FUNCT_1:def_3; hence x in union (rng F) by A31, TARSKI:def_4; ::_thesis: verum end; union (rng F) c= A /\ (less_dom ((f + g),(R_EAL r))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng F) or x in A /\ (less_dom ((f + g),(R_EAL r))) ) assume x in union (rng F) ; ::_thesis: x in A /\ (less_dom ((f + g),(R_EAL r))) then consider Y being set such that A32: x in Y and A33: Y in rng F by TARSKI:def_4; consider p being set such that A34: p in dom F and A35: Y = F . p by A33, FUNCT_1:def_3; reconsider p = p as Rational by A34; A36: x in (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A3, A32, A35; then A37: x in A /\ (less_dom (f,(R_EAL p))) by XBOOLE_0:def_4; A38: x in A /\ (less_dom (g,(R_EAL (r - p)))) by A36, XBOOLE_0:def_4; A39: x in A by A37, XBOOLE_0:def_4; A40: x in less_dom (f,(R_EAL p)) by A37, XBOOLE_0:def_4; A41: x in less_dom (g,(R_EAL (r - p))) by A38, XBOOLE_0:def_4; A42: x in dom f by A40, MESFUNC1:def_11; A43: x in dom g by A41, MESFUNC1:def_11; reconsider x = x as Element of X by A36; A44: g . x < R_EAL (r - p) by A41, MESFUNC1:def_11; A45: |.(f . x).| < +infty by A1, A42, Def1; A46: |.(g . x).| < +infty by A2, A43, Def1; A47: - +infty < f . x by A45, EXTREAL2:10; A48: - +infty < g . x by A46, EXTREAL2:10; A49: -infty < f . x by A47, XXREAL_3:23; A50: f . x < +infty by A45, EXTREAL2:10; A51: -infty < g . x by A48, XXREAL_3:23; A52: g . x < +infty by A46, EXTREAL2:10; reconsider f1 = f . x as Real by A49, A50, XXREAL_0:14; reconsider g1 = g . x as Real by A51, A52, XXREAL_0:14; A53: f1 < p by A40, MESFUNC1:def_11; p < r - g1 by A44, XREAL_1:12; then f1 < r - g1 by A53, XXREAL_0:2; then A54: f1 + g1 < r by XREAL_1:20; A55: x in dom (f + g) by A4, A42, A43, XBOOLE_0:def_4; then (f + g) . x = (f . x) + (g . x) by MESFUNC1:def_3 .= f1 + g1 by SUPINF_2:1 ; then x in less_dom ((f + g),(R_EAL r)) by A54, A55, MESFUNC1:def_11; hence x in A /\ (less_dom ((f + g),(R_EAL r))) by A39, XBOOLE_0:def_4; ::_thesis: verum end; hence A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F) by A5, XBOOLE_0:def_10; ::_thesis: verum end; begin theorem :: MESFUNC2:4 ex F being Function of NAT,RAT st ( F is one-to-one & dom F = NAT & rng F = RAT ) proof consider F being Function such that A1: F is one-to-one and A2: ( dom F = NAT & rng F = RAT ) by MESFUNC1:5, WELLORD2:def_4; F is Function of NAT,RAT by A2, FUNCT_2:2; hence ex F being Function of NAT,RAT st ( F is one-to-one & dom F = NAT & rng F = RAT ) by A1, A2; ::_thesis: verum end; theorem Th5: :: MESFUNC2:5 for X, Y, Z being non empty set for F being Function of X,Z st X,Y are_equipotent holds ex G being Function of Y,Z st rng F = rng G proof let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Z st X,Y are_equipotent holds ex G being Function of Y,Z st rng F = rng G let F be Function of X,Z; ::_thesis: ( X,Y are_equipotent implies ex G being Function of Y,Z st rng F = rng G ) assume X,Y are_equipotent ; ::_thesis: ex G being Function of Y,Z st rng F = rng G then consider H being Function such that A1: H is one-to-one and A2: dom H = Y and A3: rng H = X by WELLORD2:def_4; reconsider H = H as Function of Y,X by A2, A3, FUNCT_2:2; reconsider G = F * H as Function of Y,Z ; A4: dom F = X by FUNCT_2:def_1; A5: dom G = Y by FUNCT_2:def_1; for z being Element of Z st z in rng F holds z in rng G proof let z be Element of Z; ::_thesis: ( z in rng F implies z in rng G ) assume z in rng F ; ::_thesis: z in rng G then consider x being set such that A6: x in dom F and A7: z = F . x by FUNCT_1:def_3; x in rng H by A3, A6; then x in dom (H ") by A1, FUNCT_1:32; then (H ") . x in rng (H ") by FUNCT_1:def_3; then A8: (H ") . x in dom G by A1, A2, A5, FUNCT_1:33; then G . ((H ") . x) in rng G by FUNCT_1:def_3; then F . (H . ((H ") . x)) in rng G by A8, FUNCT_1:12; hence z in rng G by A1, A3, A6, A7, FUNCT_1:35; ::_thesis: verum end; then A9: rng F c= rng G by SUBSET_1:2; for z being Element of Z st z in rng G holds z in rng F proof let z be Element of Z; ::_thesis: ( z in rng G implies z in rng F ) assume z in rng G ; ::_thesis: z in rng F then consider y being set such that A10: y in dom G and A11: z = G . y by FUNCT_1:def_3; y in rng (H ") by A1, A2, A5, A10, FUNCT_1:33; then consider x being set such that A12: x in dom (H ") and A13: y = (H ") . x by FUNCT_1:def_3; A14: x in rng H by A1, A12, FUNCT_1:33; then A15: F . x in rng F by A4, FUNCT_1:def_3; x = H . y by A1, A13, A14, FUNCT_1:32; hence z in rng F by A10, A11, A15, FUNCT_1:12; ::_thesis: verum end; then rng G c= rng F by SUBSET_1:2; then rng F = rng G by A9, XBOOLE_0:def_10; hence ex G being Function of Y,Z st rng F = rng G ; ::_thesis: verum end; theorem Th6: :: MESFUNC2:6 for X being non empty set for r being Real for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) proof let X be non empty set ; ::_thesis: for r being Real for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) let r be Real; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) let f, g be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) let A be Element of S; ::_thesis: ( f is_measurable_on A & g is_measurable_on A implies ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) assume A1: ( f is_measurable_on A & g is_measurable_on A ) ; ::_thesis: ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) defpred S1[ set , set ] means ex p being Rational st ( p = $1 & $2 = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ); A2: for x1 being set st x1 in RAT holds ex y1 being set st ( y1 in S & S1[x1,y1] ) proof let x1 be set ; ::_thesis: ( x1 in RAT implies ex y1 being set st ( y1 in S & S1[x1,y1] ) ) assume x1 in RAT ; ::_thesis: ex y1 being set st ( y1 in S & S1[x1,y1] ) then consider p being Rational such that A3: p = x1 ; A4: ( A /\ (less_dom (f,(R_EAL p))) in S & A /\ (less_dom (g,(R_EAL (r - p)))) in S ) by A1, MESFUNC1:def_16; take (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ; ::_thesis: ( (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) in S & S1[x1,(A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))] ) thus ( (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) in S & S1[x1,(A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p)))))] ) by A3, A4, FINSUB_1:def_2; ::_thesis: verum end; consider G being Function of RAT,S such that A5: for x1 being set st x1 in RAT holds S1[x1,G . x1] from FUNCT_2:sch_1(A2); A6: for p being Rational holds G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) proof let p be Rational; ::_thesis: G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) p in RAT by RAT_1:def_2; then ex q being Rational st ( q = p & G . p = (A /\ (less_dom (f,(R_EAL q)))) /\ (A /\ (less_dom (g,(R_EAL (r - q))))) ) by A5; hence G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ; ::_thesis: verum end; take G ; ::_thesis: for p being Rational holds G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) thus for p being Rational holds G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A6; ::_thesis: verum end; theorem Th7: :: MESFUNC2:7 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A holds f + g is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A holds f + g is_measurable_on A let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A holds f + g is_measurable_on A let f, g be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A holds f + g is_measurable_on A let A be Element of S; ::_thesis: ( f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A ) assume that A1: ( f is V75() & g is V75() ) and A2: ( f is_measurable_on A & g is_measurable_on A ) ; ::_thesis: f + g is_measurable_on A for r being real number holds A /\ (less_dom ((f + g),(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (less_dom ((f + g),(R_EAL r))) in S reconsider r = r as Real by XREAL_0:def_1; consider F being Function of RAT,S such that A3: for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A2, Th6; consider G being Function of NAT,S such that A4: rng F = rng G by Th5, MESFUNC1:5; A /\ (less_dom ((f + g),(R_EAL r))) = union (rng G) by A1, A3, A4, Th3; hence A /\ (less_dom ((f + g),(R_EAL r))) in S ; ::_thesis: verum end; hence f + g is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum end; theorem Th8: :: MESFUNC2:8 for C being non empty set for f1, f2 being PartFunc of C,ExtREAL holds f1 - f2 = f1 + (- f2) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,ExtREAL holds f1 - f2 = f1 + (- f2) let f1, f2 be PartFunc of C,ExtREAL; ::_thesis: f1 - f2 = f1 + (- f2) A1: dom (f1 - f2) = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by MESFUNC1:def_4; for x being Element of C st x in f2 " {+infty} holds x in (- f2) " {-infty} proof let x be Element of C; ::_thesis: ( x in f2 " {+infty} implies x in (- f2) " {-infty} ) assume A2: x in f2 " {+infty} ; ::_thesis: x in (- f2) " {-infty} then A3: x in dom f2 by FUNCT_1:def_7; A4: f2 . x in {+infty} by A2, FUNCT_1:def_7; A5: x in dom (- f2) by A3, MESFUNC1:def_7; f2 . x = +infty by A4, TARSKI:def_1; then (- f2) . x = - +infty by A5, MESFUNC1:def_7 .= -infty by XXREAL_3:def_3 ; then (- f2) . x in {-infty} by TARSKI:def_1; hence x in (- f2) " {-infty} by A5, FUNCT_1:def_7; ::_thesis: verum end; then A6: f2 " {+infty} c= (- f2) " {-infty} by SUBSET_1:2; for x being Element of C st x in (- f2) " {-infty} holds x in f2 " {+infty} proof let x be Element of C; ::_thesis: ( x in (- f2) " {-infty} implies x in f2 " {+infty} ) assume A7: x in (- f2) " {-infty} ; ::_thesis: x in f2 " {+infty} then A8: x in dom (- f2) by FUNCT_1:def_7; A9: (- f2) . x in {-infty} by A7, FUNCT_1:def_7; A10: x in dom f2 by A8, MESFUNC1:def_7; (- f2) . x = -infty by A9, TARSKI:def_1; then -infty = - (f2 . x) by A8, MESFUNC1:def_7; then f2 . x in {+infty} by TARSKI:def_1, XXREAL_3:5; hence x in f2 " {+infty} by A10, FUNCT_1:def_7; ::_thesis: verum end; then (- f2) " {-infty} c= f2 " {+infty} by SUBSET_1:2; then A11: f2 " {+infty} = (- f2) " {-infty} by A6, XBOOLE_0:def_10; for x being Element of C st x in f2 " {-infty} holds x in (- f2) " {+infty} proof let x be Element of C; ::_thesis: ( x in f2 " {-infty} implies x in (- f2) " {+infty} ) assume A12: x in f2 " {-infty} ; ::_thesis: x in (- f2) " {+infty} then A13: x in dom f2 by FUNCT_1:def_7; A14: f2 . x in {-infty} by A12, FUNCT_1:def_7; A15: x in dom (- f2) by A13, MESFUNC1:def_7; f2 . x = -infty by A14, TARSKI:def_1; then (- f2) . x = +infty by A15, MESFUNC1:def_7, XXREAL_3:5; then (- f2) . x in {+infty} by TARSKI:def_1; hence x in (- f2) " {+infty} by A15, FUNCT_1:def_7; ::_thesis: verum end; then A16: f2 " {-infty} c= (- f2) " {+infty} by SUBSET_1:2; for x being Element of C st x in (- f2) " {+infty} holds x in f2 " {-infty} proof let x be Element of C; ::_thesis: ( x in (- f2) " {+infty} implies x in f2 " {-infty} ) assume A17: x in (- f2) " {+infty} ; ::_thesis: x in f2 " {-infty} then A18: x in dom (- f2) by FUNCT_1:def_7; A19: (- f2) . x in {+infty} by A17, FUNCT_1:def_7; A20: x in dom f2 by A18, MESFUNC1:def_7; (- f2) . x = +infty by A19, TARSKI:def_1; then +infty = - (f2 . x) by A18, MESFUNC1:def_7; then f2 . x = - +infty .= -infty by XXREAL_3:def_3 ; then f2 . x in {-infty} by TARSKI:def_1; hence x in f2 " {-infty} by A20, FUNCT_1:def_7; ::_thesis: verum end; then (- f2) " {+infty} c= f2 " {-infty} by SUBSET_1:2; then A21: f2 " {-infty} = (- f2) " {+infty} by A16, XBOOLE_0:def_10; dom (f1 + (- f2)) = ((dom f1) /\ (dom (- f2))) \ (((f1 " {-infty}) /\ ((- f2) " {+infty})) \/ ((f1 " {+infty}) /\ ((- f2) " {-infty}))) by MESFUNC1:def_3 .= ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {-infty})) \/ ((f1 " {+infty}) /\ (f2 " {+infty}))) by A11, A21, MESFUNC1:def_7 ; then A22: dom (f1 - f2) = dom (f1 + (- f2)) by MESFUNC1:def_4; for x being Element of C st x in dom (f1 - f2) holds (f1 - f2) . x = (f1 + (- f2)) . x proof let x be Element of C; ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (f1 + (- f2)) . x ) assume A23: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (f1 + (- f2)) . x dom (f1 - f2) c= (dom f1) /\ (dom f2) by A1, XBOOLE_1:36; then x in dom f2 by A23, XBOOLE_0:def_4; then A24: x in dom (- f2) by MESFUNC1:def_7; ( (f1 - f2) . x = (f1 . x) - (f2 . x) & (f1 + (- f2)) . x = (f1 . x) + ((- f2) . x) ) by A22, A23, MESFUNC1:def_3, MESFUNC1:def_4; hence (f1 - f2) . x = (f1 + (- f2)) . x by A24, MESFUNC1:def_7; ::_thesis: verum end; hence f1 - f2 = f1 + (- f2) by A22, PARTFUN1:5; ::_thesis: verum end; theorem Th9: :: MESFUNC2:9 for C being non empty set for f being PartFunc of C,ExtREAL holds - f = (- 1) (#) f proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds - f = (- 1) (#) f let f be PartFunc of C,ExtREAL; ::_thesis: - f = (- 1) (#) f A1: dom (- f) = dom f by MESFUNC1:def_7; A2: dom ((- 1) (#) f) = dom f by MESFUNC1:def_6; for x being Element of C st x in dom f holds (- f) . x = ((- 1) (#) f) . x proof let x be Element of C; ::_thesis: ( x in dom f implies (- f) . x = ((- 1) (#) f) . x ) assume A3: x in dom f ; ::_thesis: (- f) . x = ((- 1) (#) f) . x then ((- 1) (#) f) . x = (R_EAL (- 1)) * (f . x) by A2, MESFUNC1:def_6; then ((- 1) (#) f) . x = (- (R_EAL 1)) * (f . x) by SUPINF_2:2 .= - ((R_EAL 1) * (f . x)) by XXREAL_3:92 .= - (f . x) by XXREAL_3:81 ; hence (- f) . x = ((- 1) (#) f) . x by A1, A3, MESFUNC1:def_7; ::_thesis: verum end; hence - f = (- 1) (#) f by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem Th10: :: MESFUNC2:10 for C being non empty set for f being PartFunc of C,ExtREAL for r being Real st f is V75() holds r (#) f is V75() proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for r being Real st f is V75() holds r (#) f is V75() let f be PartFunc of C,ExtREAL; ::_thesis: for r being Real st f is V75() holds r (#) f is V75() let r be Real; ::_thesis: ( f is V75() implies r (#) f is V75() ) assume A1: f is V75() ; ::_thesis: r (#) f is V75() for x being Element of C st x in dom (r (#) f) holds |.((r (#) f) . x).| < +infty proof let x be Element of C; ::_thesis: ( x in dom (r (#) f) implies |.((r (#) f) . x).| < +infty ) assume A2: x in dom (r (#) f) ; ::_thesis: |.((r (#) f) . x).| < +infty then x in dom f by MESFUNC1:def_6; then A3: |.(f . x).| < +infty by A1, Def1; then - +infty < f . x by EXTREAL2:10; then A4: -infty < f . x by XXREAL_3:def_3; f . x < +infty by A3, EXTREAL2:10; then reconsider y = f . x as Real by A4, XXREAL_0:14; A5: -infty < R_EAL (r * y) by XXREAL_0:12; A6: R_EAL (r * y) < +infty by XXREAL_0:9; A7: -infty < (R_EAL r) * (R_EAL y) by A5, EXTREAL1:5; A8: (R_EAL r) * (R_EAL y) = (r (#) f) . x by A2, MESFUNC1:def_6; then A9: - +infty < (r (#) f) . x by A7, XXREAL_3:def_3; (r (#) f) . x < +infty by A6, A8, EXTREAL1:5; hence |.((r (#) f) . x).| < +infty by A9, EXTREAL2:11; ::_thesis: verum end; hence r (#) f is V75() by Def1; ::_thesis: verum end; theorem :: MESFUNC2:11 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A & A c= dom g holds f - g is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A & A c= dom g holds f - g is_measurable_on A let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A & A c= dom g holds f - g is_measurable_on A let f, g be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A & A c= dom g holds f - g is_measurable_on A let A be Element of S; ::_thesis: ( f is V75() & g is V75() & f is_measurable_on A & g is_measurable_on A & A c= dom g implies f - g is_measurable_on A ) assume that A1: f is V75() and A2: g is V75() and A3: f is_measurable_on A and A4: ( g is_measurable_on A & A c= dom g ) ; ::_thesis: f - g is_measurable_on A A5: (- 1) (#) g is V75() by A2, Th10; A6: (- 1) (#) g is_measurable_on A by A4, MESFUNC1:37; A7: - g is V75() by A5, Th9; - g is_measurable_on A by A6, Th9; then f + (- g) is_measurable_on A by A1, A3, A7, Th7; hence f - g is_measurable_on A by Th8; ::_thesis: verum end; begin definition let C be non empty set ; let f be PartFunc of C,ExtREAL; deffunc H1( Element of C) -> Element of ExtREAL = max ((f . $1),0.); func max+ f -> PartFunc of C,ExtREAL means :Def2: :: MESFUNC2:def 2 ( dom it = dom f & ( for x being Element of C st x in dom it holds it . x = max ((f . x),0.) ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds b1 . x = max ((f . x),0.) ) ) proof defpred S1[ Element of C] means $1 in dom f; consider F being PartFunc of C,ExtREAL such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F . c = H1(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = dom f & ( for x being Element of C st x in dom F holds F . x = max ((f . x),0.) ) ) thus dom F = dom f ::_thesis: for x being Element of C st x in dom F holds F . x = max ((f . x),0.) proof thus dom F c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in dom f ) assume x in dom F ; ::_thesis: x in dom f hence x in dom f by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom F ) assume x in dom f ; ::_thesis: x in dom F hence x in dom F by A1; ::_thesis: verum end; let c be Element of C; ::_thesis: ( c in dom F implies F . c = max ((f . c),0.) ) assume c in dom F ; ::_thesis: F . c = max ((f . c),0.) hence F . c = max ((f . c),0.) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds b1 . x = max ((f . x),0.) ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds b2 . x = max ((f . x),0.) ) holds b1 = b2 proof set X = dom f; thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds F . c = H1(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds G . c = H1(c) ) holds F = G from SEQ_1:sch_4(); ::_thesis: verum end; deffunc H2( Element of C) -> Element of ExtREAL = max ((- (f . $1)),0.); func max- f -> PartFunc of C,ExtREAL means :Def3: :: MESFUNC2:def 3 ( dom it = dom f & ( for x being Element of C st x in dom it holds it . x = max ((- (f . x)),0.) ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds b1 . x = max ((- (f . x)),0.) ) ) proof defpred S1[ Element of C] means $1 in dom f; consider F being PartFunc of C,ExtREAL such that A3: for c being Element of C holds ( c in dom F iff S1[c] ) and A4: for c being Element of C st c in dom F holds F . c = H2(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = dom f & ( for x being Element of C st x in dom F holds F . x = max ((- (f . x)),0.) ) ) thus dom F = dom f ::_thesis: for x being Element of C st x in dom F holds F . x = max ((- (f . x)),0.) proof thus dom F c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= dom F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in dom f ) assume x in dom F ; ::_thesis: x in dom f hence x in dom f by A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in dom F ) assume x in dom f ; ::_thesis: x in dom F hence x in dom F by A3; ::_thesis: verum end; let c be Element of C; ::_thesis: ( c in dom F implies F . c = max ((- (f . c)),0.) ) assume c in dom F ; ::_thesis: F . c = max ((- (f . c)),0.) hence F . c = max ((- (f . c)),0.) by A4; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds b1 . x = max ((- (f . x)),0.) ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds b2 . x = max ((- (f . x)),0.) ) holds b1 = b2 proof set X = dom f; thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds F . c = H2(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds G . c = H2(c) ) holds F = G from SEQ_1:sch_4(); ::_thesis: verum end; end; :: deftheorem Def2 defines max+ MESFUNC2:def_2_:_ for C being non empty set for f, b3 being PartFunc of C,ExtREAL holds ( b3 = max+ f iff ( dom b3 = dom f & ( for x being Element of C st x in dom b3 holds b3 . x = max ((f . x),0.) ) ) ); :: deftheorem Def3 defines max- MESFUNC2:def_3_:_ for C being non empty set for f, b3 being PartFunc of C,ExtREAL holds ( b3 = max- f iff ( dom b3 = dom f & ( for x being Element of C st x in dom b3 holds b3 . x = max ((- (f . x)),0.) ) ) ); theorem Th12: :: MESFUNC2:12 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C holds 0. <= (max+ f) . x proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C holds 0. <= (max+ f) . x let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C holds 0. <= (max+ f) . x let x be Element of C; ::_thesis: 0. <= (max+ f) . x A1: dom (max+ f) = dom f by Def2; percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: 0. <= (max+ f) . x then (max+ f) . x = max ((f . x),0.) by A1, Def2; hence 0. <= (max+ f) . x by XXREAL_0:25; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: 0. <= (max+ f) . x hence 0. <= (max+ f) . x by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem Th13: :: MESFUNC2:13 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C holds 0. <= (max- f) . x proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C holds 0. <= (max- f) . x let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C holds 0. <= (max- f) . x let x be Element of C; ::_thesis: 0. <= (max- f) . x A1: dom (max- f) = dom f by Def3; percases ( x in dom f or not x in dom f ) ; suppose x in dom f ; ::_thesis: 0. <= (max- f) . x then (max- f) . x = max ((- (f . x)),0.) by A1, Def3; hence 0. <= (max- f) . x by XXREAL_0:25; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: 0. <= (max- f) . x hence 0. <= (max- f) . x by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem :: MESFUNC2:14 for C being non empty set for f being PartFunc of C,ExtREAL holds max- f = max+ (- f) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds max- f = max+ (- f) let f be PartFunc of C,ExtREAL; ::_thesis: max- f = max+ (- f) A1: dom (max- f) = dom f by Def3 .= dom (- f) by MESFUNC1:def_7 ; then A2: dom (max- f) = dom (max+ (- f)) by Def2; for x being Element of C st x in dom (max- f) holds (max- f) . x = (max+ (- f)) . x proof let x be Element of C; ::_thesis: ( x in dom (max- f) implies (max- f) . x = (max+ (- f)) . x ) assume A3: x in dom (max- f) ; ::_thesis: (max- f) . x = (max+ (- f)) . x then ( (max- f) . x = max ((- (f . x)),0.) & - (f . x) = (- f) . x ) by A1, Def3, MESFUNC1:def_7; hence (max- f) . x = (max+ (- f)) . x by A2, A3, Def2; ::_thesis: verum end; hence max- f = max+ (- f) by A2, PARTFUN1:5; ::_thesis: verum end; theorem Th15: :: MESFUNC2:15 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C st 0. < (max+ f) . x holds (max- f) . x = 0. proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C st 0. < (max+ f) . x holds (max- f) . x = 0. let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st 0. < (max+ f) . x holds (max- f) . x = 0. let x be Element of C; ::_thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. ) A1: dom (max+ f) = dom f by Def2; percases ( x in dom f or not x in dom f ) ; supposeA2: x in dom f ; ::_thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. ) assume A3: 0. < (max+ f) . x ; ::_thesis: (max- f) . x = 0. A4: x in dom (max+ f) by A2, Def2; A5: x in dom (max- f) by A2, Def3; (max+ f) . x = max ((f . x),0.) by A4, Def2; then ( not f . x <= 0. or not 0. <= 0. ) by A3, XXREAL_0:28; then max ((- (f . x)),0.) = 0. by XXREAL_0:def_10; hence (max- f) . x = 0. by A5, Def3; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: ( 0. < (max+ f) . x implies (max- f) . x = 0. ) hence ( 0. < (max+ f) . x implies (max- f) . x = 0. ) by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem :: MESFUNC2:16 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C st 0. < (max- f) . x holds (max+ f) . x = 0. proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C st 0. < (max- f) . x holds (max+ f) . x = 0. let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st 0. < (max- f) . x holds (max+ f) . x = 0. let x be Element of C; ::_thesis: ( 0. < (max- f) . x implies (max+ f) . x = 0. ) A1: dom (max- f) = dom f by Def3; percases ( x in dom f or not x in dom f ) ; supposeA2: x in dom f ; ::_thesis: ( 0. < (max- f) . x implies (max+ f) . x = 0. ) assume A3: 0. < (max- f) . x ; ::_thesis: (max+ f) . x = 0. A4: x in dom (max- f) by A2, Def3; A5: x in dom (max+ f) by A2, Def2; (max- f) . x = max ((- (f . x)),0.) by A4, Def3; then - (- (f . x)) < - 0. by A3, XXREAL_0:28; then max ((f . x),0.) = 0. by XXREAL_0:def_10; hence (max+ f) . x = 0. by A5, Def2; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: ( 0. < (max- f) . x implies (max+ f) . x = 0. ) hence ( 0. < (max- f) . x implies (max+ f) . x = 0. ) by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem Th17: :: MESFUNC2:17 for C being non empty set for f being PartFunc of C,ExtREAL holds ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) let f be PartFunc of C,ExtREAL; ::_thesis: ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) A1: ( dom (max+ f) = dom f & dom (max- f) = dom f ) by Def2, Def3; (max+ f) " {+infty} misses (max- f) " {+infty} proof assume not (max+ f) " {+infty} misses (max- f) " {+infty} ; ::_thesis: contradiction then consider x1 being set such that A2: x1 in (max+ f) " {+infty} and A3: x1 in (max- f) " {+infty} by XBOOLE_0:3; reconsider x1 = x1 as Element of C by A2; A4: (max+ f) . x1 in {+infty} by A2, FUNCT_1:def_7; A5: (max- f) . x1 in {+infty} by A3, FUNCT_1:def_7; A6: (max+ f) . x1 = +infty by A4, TARSKI:def_1; (max- f) . x1 = +infty by A5, TARSKI:def_1; hence contradiction by A6, Th15; ::_thesis: verum end; then A7: ((max+ f) " {+infty}) /\ ((max- f) " {+infty}) = {} by XBOOLE_0:def_7; (max+ f) " {-infty} misses (max- f) " {-infty} proof assume not (max+ f) " {-infty} misses (max- f) " {-infty} ; ::_thesis: contradiction then consider x1 being set such that A8: x1 in (max+ f) " {-infty} and x1 in (max- f) " {-infty} by XBOOLE_0:3; reconsider x1 = x1 as Element of C by A8; (max+ f) . x1 in {-infty} by A8, FUNCT_1:def_7; then (max+ f) . x1 = -infty by TARSKI:def_1; hence contradiction by Th12; ::_thesis: verum end; then A9: ((max+ f) " {-infty}) /\ ((max- f) " {-infty}) = {} by XBOOLE_0:def_7; (max+ f) " {+infty} misses (max- f) " {-infty} proof assume not (max+ f) " {+infty} misses (max- f) " {-infty} ; ::_thesis: contradiction then consider x1 being set such that A10: x1 in (max+ f) " {+infty} and A11: x1 in (max- f) " {-infty} by XBOOLE_0:3; reconsider x1 = x1 as Element of C by A10; (max- f) . x1 in {-infty} by A11, FUNCT_1:def_7; then (max- f) . x1 = -infty by TARSKI:def_1; hence contradiction by Th13; ::_thesis: verum end; then A12: ((max+ f) " {+infty}) /\ ((max- f) " {-infty}) = {} by XBOOLE_0:def_7; (max+ f) " {-infty} misses (max- f) " {+infty} proof assume not (max+ f) " {-infty} misses (max- f) " {+infty} ; ::_thesis: contradiction then consider x1 being set such that A13: x1 in (max+ f) " {-infty} and x1 in (max- f) " {+infty} by XBOOLE_0:3; reconsider x1 = x1 as Element of C by A13; (max+ f) . x1 in {-infty} by A13, FUNCT_1:def_7; then (max+ f) . x1 = -infty by TARSKI:def_1; hence contradiction by Th12; ::_thesis: verum end; then A14: ((max+ f) " {-infty}) /\ ((max- f) " {+infty}) = {} by XBOOLE_0:def_7; dom ((max+ f) - (max- f)) = ((dom f) /\ (dom f)) \ ({} \/ {}) by A1, A7, A9, MESFUNC1:def_4; hence ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) by A1, A12, A14, MESFUNC1:def_3; ::_thesis: verum end; theorem Th18: :: MESFUNC2:18 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C holds ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C holds ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C holds ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) let x be Element of C; ::_thesis: ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) A1: ( dom (max- f) = dom f & dom (max+ f) = dom f ) by Def2, Def3; percases ( x in dom f or not x in dom f ) ; supposeA2: x in dom f ; ::_thesis: ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) then A3: x in dom (max+ f) by Def2; A4: x in dom (max- f) by A2, Def3; A5: (max+ f) . x = max ((f . x),0.) by A3, Def2; (max- f) . x = max ((- (f . x)),0.) by A4, Def3; hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by A5, XXREAL_0:16; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) hence ( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) ) by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem Th19: :: MESFUNC2:19 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C st (max+ f) . x = f . x holds (max- f) . x = 0. proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C st (max+ f) . x = f . x holds (max- f) . x = 0. let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st (max+ f) . x = f . x holds (max- f) . x = 0. let x be Element of C; ::_thesis: ( (max+ f) . x = f . x implies (max- f) . x = 0. ) A1: dom (max- f) = dom f by Def3; percases ( x in dom f or not x in dom f ) ; supposeA2: x in dom f ; ::_thesis: ( (max+ f) . x = f . x implies (max- f) . x = 0. ) assume A3: (max+ f) . x = f . x ; ::_thesis: (max- f) . x = 0. A4: x in dom (max+ f) by A2, Def2; A5: x in dom (max- f) by A2, Def3; A6: (max+ f) . x = max ((f . x),0.) by A4, Def2; A7: (max- f) . x = max ((- (f . x)),0.) by A5, Def3; 0. <= f . x by A3, A6, XXREAL_0:def_10; hence (max- f) . x = 0. by A7, XXREAL_0:def_10; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: ( (max+ f) . x = f . x implies (max- f) . x = 0. ) hence ( (max+ f) . x = f . x implies (max- f) . x = 0. ) by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem Th20: :: MESFUNC2:20 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C st x in dom f & (max+ f) . x = 0. holds (max- f) . x = - (f . x) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C st x in dom f & (max+ f) . x = 0. holds (max- f) . x = - (f . x) let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st x in dom f & (max+ f) . x = 0. holds (max- f) . x = - (f . x) let x be Element of C; ::_thesis: ( x in dom f & (max+ f) . x = 0. implies (max- f) . x = - (f . x) ) assume that A1: x in dom f and A2: (max+ f) . x = 0. ; ::_thesis: (max- f) . x = - (f . x) A3: x in dom (max+ f) by A1, Def2; A4: x in dom (max- f) by A1, Def3; A5: (max+ f) . x = max ((f . x),0.) by A3, Def2; A6: (max- f) . x = max ((- (f . x)),0.) by A4, Def3; f . x <= 0. by A2, A5, XXREAL_0:def_10; hence (max- f) . x = - (f . x) by A6, XXREAL_0:def_10; ::_thesis: verum end; theorem :: MESFUNC2:21 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C st (max- f) . x = - (f . x) holds (max+ f) . x = 0. proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C st (max- f) . x = - (f . x) holds (max+ f) . x = 0. let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st (max- f) . x = - (f . x) holds (max+ f) . x = 0. let x be Element of C; ::_thesis: ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. ) A1: dom (max+ f) = dom f by Def2; percases ( x in dom f or not x in dom f ) ; supposeA2: x in dom f ; ::_thesis: ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. ) assume A3: (max- f) . x = - (f . x) ; ::_thesis: (max+ f) . x = 0. A4: x in dom (max+ f) by A2, Def2; A5: x in dom (max- f) by A2, Def3; A6: (max+ f) . x = max ((f . x),0.) by A4, Def2; (max- f) . x = max ((- (f . x)),0.) by A5, Def3; then - (- (f . x)) <= - 0. by A3, XXREAL_0:def_10; hence (max+ f) . x = 0. by A6, XXREAL_0:def_10; ::_thesis: verum end; suppose not x in dom f ; ::_thesis: ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. ) hence ( (max- f) . x = - (f . x) implies (max+ f) . x = 0. ) by A1, FUNCT_1:def_2; ::_thesis: verum end; end; end; theorem :: MESFUNC2:22 for C being non empty set for f being PartFunc of C,ExtREAL for x being Element of C st x in dom f & (max- f) . x = 0. holds (max+ f) . x = f . x proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for x being Element of C st x in dom f & (max- f) . x = 0. holds (max+ f) . x = f . x let f be PartFunc of C,ExtREAL; ::_thesis: for x being Element of C st x in dom f & (max- f) . x = 0. holds (max+ f) . x = f . x let x be Element of C; ::_thesis: ( x in dom f & (max- f) . x = 0. implies (max+ f) . x = f . x ) assume that A1: x in dom f and A2: (max- f) . x = 0. ; ::_thesis: (max+ f) . x = f . x A3: x in dom (max+ f) by A1, Def2; A4: x in dom (max- f) by A1, Def3; A5: (max+ f) . x = max ((f . x),0.) by A3, Def2; (max- f) . x = max ((- (f . x)),0.) by A4, Def3; then - 0. <= - (- (f . x)) by A2, XXREAL_0:def_10; hence (max+ f) . x = f . x by A5, XXREAL_0:def_10; ::_thesis: verum end; theorem :: MESFUNC2:23 for C being non empty set for f being PartFunc of C,ExtREAL holds f = (max+ f) - (max- f) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds f = (max+ f) - (max- f) let f be PartFunc of C,ExtREAL; ::_thesis: f = (max+ f) - (max- f) A1: dom f = dom ((max+ f) - (max- f)) by Th17; for x being Element of C st x in dom f holds f . x = ((max+ f) - (max- f)) . x proof let x be Element of C; ::_thesis: ( x in dom f implies f . x = ((max+ f) - (max- f)) . x ) assume A2: x in dom f ; ::_thesis: f . x = ((max+ f) - (max- f)) . x then A3: ((max+ f) - (max- f)) . x = ((max+ f) . x) - ((max- f) . x) by A1, MESFUNC1:def_4; percases ( (max+ f) . x = f . x or (max+ f) . x = 0. ) by Th18; supposeA4: (max+ f) . x = f . x ; ::_thesis: f . x = ((max+ f) - (max- f)) . x then (max- f) . x = 0. by Th19; then - ((max- f) . x) = 0 ; hence f . x = ((max+ f) - (max- f)) . x by A3, A4, XXREAL_3:4; ::_thesis: verum end; supposeA5: (max+ f) . x = 0. ; ::_thesis: f . x = ((max+ f) - (max- f)) . x then (max- f) . x = - (f . x) by A2, Th20; hence f . x = ((max+ f) - (max- f)) . x by A3, A5, XXREAL_3:4; ::_thesis: verum end; end; end; hence f = (max+ f) - (max- f) by A1, PARTFUN1:5; ::_thesis: verum end; theorem :: MESFUNC2:24 for C being non empty set for f being PartFunc of C,ExtREAL holds |.f.| = (max+ f) + (max- f) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds |.f.| = (max+ f) + (max- f) let f be PartFunc of C,ExtREAL; ::_thesis: |.f.| = (max+ f) + (max- f) A1: dom f = dom ((max+ f) + (max- f)) by Th17; A2: dom f = dom |.f.| by MESFUNC1:def_10; for x being Element of C st x in dom f holds |.f.| . x = ((max+ f) + (max- f)) . x proof let x be Element of C; ::_thesis: ( x in dom f implies |.f.| . x = ((max+ f) + (max- f)) . x ) assume A3: x in dom f ; ::_thesis: |.f.| . x = ((max+ f) + (max- f)) . x now__::_thesis:_|.f.|_._x_=_((max+_f)_+_(max-_f))_._x percases ( (max+ f) . x = f . x or (max+ f) . x = 0. ) by Th18; supposeA4: (max+ f) . x = f . x ; ::_thesis: |.f.| . x = ((max+ f) + (max- f)) . x then A5: ((max+ f) . x) + ((max- f) . x) = (f . x) + 0. by Th19 .= f . x by XXREAL_3:4 ; x in dom (max+ f) by A3, Def2; then (max+ f) . x = max ((f . x),0.) by Def2; then 0. <= f . x by A4, XXREAL_0:def_10; then f . x = |.(f . x).| by EXTREAL1:def_1 .= |.f.| . x by A2, A3, MESFUNC1:def_10 ; hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A3, A5, MESFUNC1:def_3; ::_thesis: verum end; supposeA6: (max+ f) . x = 0. ; ::_thesis: |.f.| . x = ((max+ f) + (max- f)) . x then A7: ((max+ f) . x) + ((max- f) . x) = 0. + (- (f . x)) by A3, Th20 .= - (f . x) by XXREAL_3:4 ; x in dom (max+ f) by A3, Def2; then (max+ f) . x = max ((f . x),0.) by Def2; then f . x <= 0. by A6, XXREAL_0:def_10; then - (f . x) = |.(f . x).| by EXTREAL2:7 .= |.f.| . x by A2, A3, MESFUNC1:def_10 ; hence |.f.| . x = ((max+ f) + (max- f)) . x by A1, A3, A7, MESFUNC1:def_3; ::_thesis: verum end; end; end; hence |.f.| . x = ((max+ f) + (max- f)) . x ; ::_thesis: verum end; hence |.f.| = (max+ f) + (max- f) by A1, A2, PARTFUN1:5; ::_thesis: verum end; begin theorem :: MESFUNC2:25 for X being non empty set for f being PartFunc of X,ExtREAL for S being SigmaField of X for A being Element of S st f is_measurable_on A holds max+ f is_measurable_on A proof 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_measurable_on A holds max+ 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_measurable_on A holds max+ f is_measurable_on A let S be SigmaField of X; ::_thesis: for A being Element of S st f is_measurable_on A holds max+ f is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A implies max+ f is_measurable_on A ) assume A1: f is_measurable_on A ; ::_thesis: max+ f is_measurable_on A for r being real number holds A /\ (less_dom ((max+ f),(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (less_dom ((max+ f),(R_EAL r))) in S reconsider r = r as Real by XREAL_0:def_1; now__::_thesis:_A_/\_(less_dom_((max+_f),(R_EAL_r)))_in_S percases ( 0 < r or r <= 0 ) ; supposeA2: 0 < r ; ::_thesis: A /\ (less_dom ((max+ f),(R_EAL r))) in S for x being set st x in less_dom ((max+ f),(R_EAL r)) holds x in less_dom (f,(R_EAL r)) proof let x be set ; ::_thesis: ( x in less_dom ((max+ f),(R_EAL r)) implies x in less_dom (f,(R_EAL r)) ) assume A3: x in less_dom ((max+ f),(R_EAL r)) ; ::_thesis: x in less_dom (f,(R_EAL r)) then A4: x in dom (max+ f) by MESFUNC1:def_11; A5: (max+ f) . x < R_EAL r by A3, MESFUNC1:def_11; reconsider x = x as Element of X by A3; A6: max ((f . x),0.) < R_EAL r by A4, A5, Def2; then A7: f . x <= R_EAL r by XXREAL_0:30; f . x <> R_EAL r proof assume A8: f . x = R_EAL r ; ::_thesis: contradiction then max ((f . x),0.) = 0. by A6, XXREAL_0:16; hence contradiction by A6, A8, XXREAL_0:def_10; ::_thesis: verum end; then A9: f . x < R_EAL r by A7, XXREAL_0:1; x in dom f by A4, Def2; hence x in less_dom (f,(R_EAL r)) by A9, MESFUNC1:def_11; ::_thesis: verum end; then A10: less_dom ((max+ f),(R_EAL r)) c= less_dom (f,(R_EAL r)) by TARSKI:def_3; for x being set st x in less_dom (f,(R_EAL r)) holds x in less_dom ((max+ f),(R_EAL r)) proof let x be set ; ::_thesis: ( x in less_dom (f,(R_EAL r)) implies x in less_dom ((max+ f),(R_EAL r)) ) assume A11: x in less_dom (f,(R_EAL r)) ; ::_thesis: x in less_dom ((max+ f),(R_EAL r)) then A12: x in dom f by MESFUNC1:def_11; A13: f . x < R_EAL r by A11, MESFUNC1:def_11; reconsider x = x as Element of X by A11; A14: x in dom (max+ f) by A12, Def2; now__::_thesis:_x_in_less_dom_((max+_f),(R_EAL_r)) percases ( 0. <= f . x or not 0. <= f . x ) ; suppose 0. <= f . x ; ::_thesis: x in less_dom ((max+ f),(R_EAL r)) then max ((f . x),0.) = f . x by XXREAL_0:def_10; then (max+ f) . x = f . x by A14, Def2; hence x in less_dom ((max+ f),(R_EAL r)) by A13, A14, MESFUNC1:def_11; ::_thesis: verum end; suppose not 0. <= f . x ; ::_thesis: x in less_dom ((max+ f),(R_EAL r)) then max ((f . x),0.) = 0. by XXREAL_0:def_10; then (max+ f) . x = 0. by A14, Def2; hence x in less_dom ((max+ f),(R_EAL r)) by A2, A14, MESFUNC1:def_11; ::_thesis: verum end; end; end; hence x in less_dom ((max+ f),(R_EAL r)) ; ::_thesis: verum end; then less_dom (f,(R_EAL r)) c= less_dom ((max+ f),(R_EAL r)) by TARSKI:def_3; then less_dom ((max+ f),(R_EAL r)) = less_dom (f,(R_EAL r)) by A10, XBOOLE_0:def_10; hence A /\ (less_dom ((max+ f),(R_EAL r))) in S by A1, MESFUNC1:def_16; ::_thesis: verum end; supposeA15: r <= 0 ; ::_thesis: A /\ (less_dom ((max+ f),(R_EAL r))) in S for x being Element of X holds not x in less_dom ((max+ f),(R_EAL r)) proof let x be Element of X; ::_thesis: not x in less_dom ((max+ f),(R_EAL r)) assume A16: x in less_dom ((max+ f),(R_EAL r)) ; ::_thesis: contradiction then A17: x in dom (max+ f) by MESFUNC1:def_11; A18: (max+ f) . x < R_EAL r by A16, MESFUNC1:def_11; (max+ f) . x = max ((f . x),0.) by A17, Def2; hence contradiction by A15, A18, XXREAL_0:25; ::_thesis: verum end; then less_dom ((max+ f),(R_EAL r)) = {} by SUBSET_1:4; hence A /\ (less_dom ((max+ f),(R_EAL r))) in S by PROB_1:4; ::_thesis: verum end; end; end; hence A /\ (less_dom ((max+ f),(R_EAL r))) in S ; ::_thesis: verum end; hence max+ f is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum end; theorem :: MESFUNC2:26 for X being non empty set for f being PartFunc of X,ExtREAL for S being SigmaField of X for A being Element of S st f is_measurable_on A & A c= dom f holds max- f is_measurable_on A proof 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_measurable_on A & A c= dom f holds max- 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_measurable_on A & A c= dom f holds max- f is_measurable_on A let S be SigmaField of X; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds max- f is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies max- f is_measurable_on A ) assume A1: ( f is_measurable_on A & A c= dom f ) ; ::_thesis: max- f is_measurable_on A for r being real number holds A /\ (less_dom ((max- f),(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (less_dom ((max- f),(R_EAL r))) in S reconsider r = r as Real by XREAL_0:def_1; now__::_thesis:_A_/\_(less_dom_((max-_f),(R_EAL_r)))_in_S percases ( 0 < r or r <= 0 ) ; supposeA2: 0 < r ; ::_thesis: A /\ (less_dom ((max- f),(R_EAL r))) in S (- 1) (#) f is_measurable_on A by A1, MESFUNC1:37; then A3: - f is_measurable_on A by Th9; for x being set st x in less_dom ((max- f),(R_EAL r)) holds x in less_dom ((- f),(R_EAL r)) proof let x be set ; ::_thesis: ( x in less_dom ((max- f),(R_EAL r)) implies x in less_dom ((- f),(R_EAL r)) ) assume A4: x in less_dom ((max- f),(R_EAL r)) ; ::_thesis: x in less_dom ((- f),(R_EAL r)) then A5: x in dom (max- f) by MESFUNC1:def_11; A6: (max- f) . x < R_EAL r by A4, MESFUNC1:def_11; reconsider x = x as Element of X by A4; A7: max ((- (f . x)),0.) < R_EAL r by A5, A6, Def3; then A8: - (f . x) <= R_EAL r by XXREAL_0:30; - (f . x) <> R_EAL r proof assume A9: - (f . x) = R_EAL r ; ::_thesis: contradiction then max ((- (f . x)),0.) = 0. by A7, XXREAL_0:16; hence contradiction by A7, A9, XXREAL_0:def_10; ::_thesis: verum end; then A10: - (f . x) < R_EAL r by A8, XXREAL_0:1; x in dom f by A5, Def3; then A11: x in dom (- f) by MESFUNC1:def_7; then (- f) . x = - (f . x) by MESFUNC1:def_7; hence x in less_dom ((- f),(R_EAL r)) by A10, A11, MESFUNC1:def_11; ::_thesis: verum end; then A12: less_dom ((max- f),(R_EAL r)) c= less_dom ((- f),(R_EAL r)) by TARSKI:def_3; for x being set st x in less_dom ((- f),(R_EAL r)) holds x in less_dom ((max- f),(R_EAL r)) proof let x be set ; ::_thesis: ( x in less_dom ((- f),(R_EAL r)) implies x in less_dom ((max- f),(R_EAL r)) ) assume A13: x in less_dom ((- f),(R_EAL r)) ; ::_thesis: x in less_dom ((max- f),(R_EAL r)) then A14: x in dom (- f) by MESFUNC1:def_11; A15: (- f) . x < R_EAL r by A13, MESFUNC1:def_11; reconsider x = x as Element of X by A13; x in dom f by A14, MESFUNC1:def_7; then A16: x in dom (max- f) by Def3; now__::_thesis:_x_in_less_dom_((max-_f),(R_EAL_r)) percases ( 0. <= - (f . x) or not 0. <= - (f . x) ) ; suppose 0. <= - (f . x) ; ::_thesis: x in less_dom ((max- f),(R_EAL r)) then max ((- (f . x)),0.) = - (f . x) by XXREAL_0:def_10; then (max- f) . x = - (f . x) by A16, Def3 .= (- f) . x by A14, MESFUNC1:def_7 ; hence x in less_dom ((max- f),(R_EAL r)) by A15, A16, MESFUNC1:def_11; ::_thesis: verum end; suppose not 0. <= - (f . x) ; ::_thesis: x in less_dom ((max- f),(R_EAL r)) then max ((- (f . x)),0.) = 0. by XXREAL_0:def_10; then (max- f) . x = 0. by A16, Def3; hence x in less_dom ((max- f),(R_EAL r)) by A2, A16, MESFUNC1:def_11; ::_thesis: verum end; end; end; hence x in less_dom ((max- f),(R_EAL r)) ; ::_thesis: verum end; then less_dom ((- f),(R_EAL r)) c= less_dom ((max- f),(R_EAL r)) by TARSKI:def_3; then less_dom ((max- f),(R_EAL r)) = less_dom ((- f),(R_EAL r)) by A12, XBOOLE_0:def_10; hence A /\ (less_dom ((max- f),(R_EAL r))) in S by A3, MESFUNC1:def_16; ::_thesis: verum end; supposeA17: r <= 0 ; ::_thesis: A /\ (less_dom ((max- f),(R_EAL r))) in S for x being Element of X holds not x in less_dom ((max- f),(R_EAL r)) proof let x be Element of X; ::_thesis: not x in less_dom ((max- f),(R_EAL r)) assume A18: x in less_dom ((max- f),(R_EAL r)) ; ::_thesis: contradiction then A19: x in dom (max- f) by MESFUNC1:def_11; A20: (max- f) . x < R_EAL r by A18, MESFUNC1:def_11; (max- f) . x = max ((- (f . x)),0.) by A19, Def3; hence contradiction by A17, A20, XXREAL_0:25; ::_thesis: verum end; then less_dom ((max- f),(R_EAL r)) = {} by SUBSET_1:4; hence A /\ (less_dom ((max- f),(R_EAL r))) in S by PROB_1:4; ::_thesis: verum end; end; end; hence A /\ (less_dom ((max- f),(R_EAL r))) in S ; ::_thesis: verum end; hence max- f is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum end; theorem :: MESFUNC2:27 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds |.f.| is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds |.f.| is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds |.f.| is_measurable_on A let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds |.f.| is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies |.f.| is_measurable_on A ) assume A1: ( f is_measurable_on A & A c= dom f ) ; ::_thesis: |.f.| is_measurable_on A for r being real number holds A /\ (less_dom (|.f.|,(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (less_dom (|.f.|,(R_EAL r))) in S reconsider r = r as Real by XREAL_0:def_1; for x being set st x in less_dom (|.f.|,(R_EAL r)) holds x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) proof let x be set ; ::_thesis: ( x in less_dom (|.f.|,(R_EAL r)) implies x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) ) assume A2: x in less_dom (|.f.|,(R_EAL r)) ; ::_thesis: x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) then A3: x in dom |.f.| by MESFUNC1:def_11; A4: |.f.| . x < R_EAL r by A2, MESFUNC1:def_11; reconsider x = x as Element of X by A2; A5: x in dom f by A3, MESFUNC1:def_10; A6: |.(f . x).| < R_EAL r by A3, A4, MESFUNC1:def_10; then A7: - (R_EAL r) < f . x by EXTREAL2:10; A8: f . x < R_EAL r by A6, EXTREAL2:10; A9: - (R_EAL r) = - r by SUPINF_2:2; A10: x in less_dom (f,(R_EAL r)) by A5, A8, MESFUNC1:def_11; x in great_dom (f,(R_EAL (- r))) by A5, A7, A9, MESFUNC1:def_13; hence x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by A10, XBOOLE_0:def_4; ::_thesis: verum end; then A11: less_dom (|.f.|,(R_EAL r)) c= (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by TARSKI:def_3; for x being set st x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) holds x in less_dom (|.f.|,(R_EAL r)) proof let x be set ; ::_thesis: ( x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) implies x in less_dom (|.f.|,(R_EAL r)) ) assume A12: x in (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) ; ::_thesis: x in less_dom (|.f.|,(R_EAL r)) then A13: x in less_dom (f,(R_EAL r)) by XBOOLE_0:def_4; A14: x in great_dom (f,(R_EAL (- r))) by A12, XBOOLE_0:def_4; A15: x in dom f by A13, MESFUNC1:def_11; A16: f . x < R_EAL r by A13, MESFUNC1:def_11; A17: R_EAL (- r) < f . x by A14, MESFUNC1:def_13; reconsider x = x as Element of X by A12; A18: x in dom |.f.| by A15, MESFUNC1:def_10; - (R_EAL r) = - r by SUPINF_2:2; then |.(f . x).| < R_EAL r by A16, A17, EXTREAL2:11; then |.f.| . x < R_EAL r by A18, MESFUNC1:def_10; hence x in less_dom (|.f.|,(R_EAL r)) by A18, MESFUNC1:def_11; ::_thesis: verum end; then (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) c= less_dom (|.f.|,(R_EAL r)) by TARSKI:def_3; then A19: less_dom (|.f.|,(R_EAL r)) = (less_dom (f,(R_EAL r))) /\ (great_dom (f,(R_EAL (- r)))) by A11, XBOOLE_0:def_10; (A /\ (great_dom (f,(R_EAL (- r))))) /\ (less_dom (f,(R_EAL r))) in S by A1, MESFUNC1:32; hence A /\ (less_dom (|.f.|,(R_EAL r))) in S by A19, XBOOLE_1:16; ::_thesis: verum end; hence |.f.| is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum end; begin definition let A, X be set ; :: original: chi redefine func chi (A,X) -> PartFunc of X,ExtREAL; coherence chi (A,X) is PartFunc of X,ExtREAL proof now__::_thesis:_for_x_being_set_st_x_in_rng_(chi_(A,X))_holds_ x_in_ExtREAL let x be set ; ::_thesis: ( x in rng (chi (A,X)) implies x in ExtREAL ) assume A1: x in rng (chi (A,X)) ; ::_thesis: x in ExtREAL now__::_thesis:_x_in_ExtREAL percases ( x = 0. or x = 1. ) by A1, MESFUNC1:def_8, TARSKI:def_2; suppose x = 0. ; ::_thesis: x in ExtREAL hence x in ExtREAL ; ::_thesis: verum end; suppose x = 1. ; ::_thesis: x in ExtREAL hence x in ExtREAL ; ::_thesis: verum end; end; end; hence x in ExtREAL ; ::_thesis: verum end; then ( dom (chi (A,X)) = X & rng (chi (A,X)) c= ExtREAL ) by FUNCT_3:def_3, TARSKI:def_3; hence chi (A,X) is PartFunc of X,ExtREAL by RELSET_1:4; ::_thesis: verum end; end; theorem :: MESFUNC2:28 for X being non empty set for S being SigmaField of X for A being Element of S holds chi (A,X) is V75() proof let X be non empty set ; ::_thesis: for S being SigmaField of X for A being Element of S holds chi (A,X) is V75() let S be SigmaField of X; ::_thesis: for A being Element of S holds chi (A,X) is V75() let A be Element of S; ::_thesis: chi (A,X) is V75() for x being Element of X st x in dom (chi (A,X)) holds |.((chi (A,X)) . x).| < +infty proof let x be Element of X; ::_thesis: ( x in dom (chi (A,X)) implies |.((chi (A,X)) . x).| < +infty ) assume x in dom (chi (A,X)) ; ::_thesis: |.((chi (A,X)) . x).| < +infty now__::_thesis:_|.((chi_(A,X))_._x).|_<_+infty percases ( x in A or not x in A ) ; suppose x in A ; ::_thesis: |.((chi (A,X)) . x).| < +infty then (chi (A,X)) . x = 1. by FUNCT_3:def_3, MESFUNC1:def_8; then |.((chi (A,X)) . x).| = 1. by EXTREAL1:def_1, MESFUNC1:def_8; hence |.((chi (A,X)) . x).| < +infty by MESFUNC1:def_8, XXREAL_0:9; ::_thesis: verum end; suppose not x in A ; ::_thesis: |.((chi (A,X)) . x).| < +infty then (chi (A,X)) . x = 0. by FUNCT_3:def_3; hence |.((chi (A,X)) . x).| < +infty by EXTREAL1:def_1; ::_thesis: verum end; end; end; hence |.((chi (A,X)) . x).| < +infty ; ::_thesis: verum end; hence chi (A,X) is V75() by Def1; ::_thesis: verum end; theorem :: MESFUNC2:29 for X being non empty set for S being SigmaField of X for A, B being Element of S holds chi (A,X) is_measurable_on B proof let X be non empty set ; ::_thesis: for S being SigmaField of X for A, B being Element of S holds chi (A,X) is_measurable_on B let S be SigmaField of X; ::_thesis: for A, B being Element of S holds chi (A,X) is_measurable_on B let A, B be Element of S; ::_thesis: chi (A,X) is_measurable_on B for r being real number holds B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S proof let r be real number ; ::_thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S reconsider r = r as Real by XREAL_0:def_1; now__::_thesis:_B_/\_(less_eq_dom_((chi_(A,X)),(R_EAL_r)))_in_S percases ( r >= 1 or ( 0 <= r & r < 1 ) or r < 0 ) ; supposeA1: r >= 1 ; ::_thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S for x being set st x in X holds x in less_eq_dom ((chi (A,X)),(R_EAL r)) proof let x be set ; ::_thesis: ( x in X implies x in less_eq_dom ((chi (A,X)),(R_EAL r)) ) assume A2: x in X ; ::_thesis: x in less_eq_dom ((chi (A,X)),(R_EAL r)) then A3: x in dom (chi (A,X)) by FUNCT_3:def_3; reconsider x = x as Element of X by A2; (chi (A,X)) . x <= 1. proof now__::_thesis:_(chi_(A,X))_._x_<=_1. percases ( x in A or not x in A ) ; suppose x in A ; ::_thesis: (chi (A,X)) . x <= 1. hence (chi (A,X)) . x <= 1. by FUNCT_3:def_3, MESFUNC1:def_8; ::_thesis: verum end; suppose not x in A ; ::_thesis: (chi (A,X)) . x <= 1. hence (chi (A,X)) . x <= 1. by FUNCT_3:def_3, MESFUNC1:def_8; ::_thesis: verum end; end; end; hence (chi (A,X)) . x <= 1. ; ::_thesis: verum end; then (chi (A,X)) . x <= R_EAL r by A1, MESFUNC1:def_8, XXREAL_0:2; hence x in less_eq_dom ((chi (A,X)),(R_EAL r)) by A3, MESFUNC1:def_12; ::_thesis: verum end; then X c= less_eq_dom ((chi (A,X)),(R_EAL r)) by TARSKI:def_3; then less_eq_dom ((chi (A,X)),(R_EAL r)) = X by XBOOLE_0:def_10; then less_eq_dom ((chi (A,X)),(R_EAL r)) in S by PROB_1:5; hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S by FINSUB_1:def_2; ::_thesis: verum end; supposeA4: ( 0 <= r & r < 1 ) ; ::_thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S for x being set st x in less_eq_dom ((chi (A,X)),(R_EAL r)) holds x in X \ A proof let x be set ; ::_thesis: ( x in less_eq_dom ((chi (A,X)),(R_EAL r)) implies x in X \ A ) assume A5: x in less_eq_dom ((chi (A,X)),(R_EAL r)) ; ::_thesis: x in X \ A then reconsider x = x as Element of X ; (chi (A,X)) . x <= R_EAL r by A5, MESFUNC1:def_12; then not x in A by A4, FUNCT_3:def_3; hence x in X \ A by XBOOLE_0:def_5; ::_thesis: verum end; then A6: less_eq_dom ((chi (A,X)),(R_EAL r)) c= X \ A by TARSKI:def_3; for x being set st x in X \ A holds x in less_eq_dom ((chi (A,X)),(R_EAL r)) proof let x be set ; ::_thesis: ( x in X \ A implies x in less_eq_dom ((chi (A,X)),(R_EAL r)) ) assume A7: x in X \ A ; ::_thesis: x in less_eq_dom ((chi (A,X)),(R_EAL r)) then A8: x in X ; A9: not x in A by A7, XBOOLE_0:def_5; reconsider x = x as Element of X by A7; A10: (chi (A,X)) . x = 0. by A9, FUNCT_3:def_3; x in dom (chi (A,X)) by A8, FUNCT_3:def_3; hence x in less_eq_dom ((chi (A,X)),(R_EAL r)) by A4, A10, MESFUNC1:def_12; ::_thesis: verum end; then X \ A c= less_eq_dom ((chi (A,X)),(R_EAL r)) by TARSKI:def_3; then A11: less_eq_dom ((chi (A,X)),(R_EAL r)) = X \ A by A6, XBOOLE_0:def_10; X in S by PROB_1:5; then less_eq_dom ((chi (A,X)),(R_EAL r)) in S by A11, MEASURE1:6; hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S by FINSUB_1:def_2; ::_thesis: verum end; supposeA12: r < 0 ; ::_thesis: B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S for x being Element of X holds not x in less_eq_dom ((chi (A,X)),(R_EAL r)) proof assume ex x being Element of X st x in less_eq_dom ((chi (A,X)),(R_EAL r)) ; ::_thesis: contradiction then consider x being Element of X such that A13: x in less_eq_dom ((chi (A,X)),(R_EAL r)) ; 0. <= (chi (A,X)) . x proof now__::_thesis:_0._<=_(chi_(A,X))_._x percases ( x in A or not x in A ) ; suppose x in A ; ::_thesis: 0. <= (chi (A,X)) . x hence 0. <= (chi (A,X)) . x by FUNCT_3:def_3; ::_thesis: verum end; suppose not x in A ; ::_thesis: 0. <= (chi (A,X)) . x hence 0. <= (chi (A,X)) . x by FUNCT_3:def_3; ::_thesis: verum end; end; end; hence 0. <= (chi (A,X)) . x ; ::_thesis: verum end; hence contradiction by A12, A13, MESFUNC1:def_12; ::_thesis: verum end; then less_eq_dom ((chi (A,X)),(R_EAL r)) = {} by SUBSET_1:4; hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S by PROB_1:4; ::_thesis: verum end; end; end; hence B /\ (less_eq_dom ((chi (A,X)),(R_EAL r))) in S ; ::_thesis: verum end; hence chi (A,X) is_measurable_on B by MESFUNC1:28; ::_thesis: verum end; begin registration let X be set ; let S be SigmaField of X; cluster Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like disjoint_valued for FinSequence of S; existence ex b1 being FinSequence of S st b1 is disjoint_valued proof reconsider A = {} as Element of S by PROB_1:4; reconsider p = (Seg 1) --> A as Function of (Seg 1),S ; A1: dom p = Seg 1 by FUNCOP_1:13; then reconsider p = p as FinSequence by FINSEQ_1:def_2; rng p c= S by RELAT_1:def_19; then reconsider p = p as FinSequence of S by FINSEQ_1:def_4; A2: for n, m being set st n <> m holds p . n misses p . m proof let n, m be set ; ::_thesis: ( n <> m implies p . n misses p . m ) assume n <> m ; ::_thesis: p . n misses p . m p . n = {} proof percases ( n in dom p or not n in dom p ) ; suppose n in dom p ; ::_thesis: p . n = {} hence p . n = {} by A1, FUNCOP_1:7; ::_thesis: verum end; suppose not n in dom p ; ::_thesis: p . n = {} hence p . n = {} by FUNCT_1:def_2; ::_thesis: verum end; end; end; hence p . n misses p . m by XBOOLE_1:65; ::_thesis: verum end; take p ; ::_thesis: p is disjoint_valued thus p is disjoint_valued by A2, PROB_2:def_2; ::_thesis: verum end; end; definition let X be set ; let S be SigmaField of X; mode Finite_Sep_Sequence of S is disjoint_valued FinSequence of S; end; theorem Th30: :: MESFUNC2:30 for X being non empty set for S being SigmaField of X for F being Function st F is Finite_Sep_Sequence of S holds ex G being Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds F . n = G . n ) & ( for m being Nat st not m in dom F holds G . m = {} ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for F being Function st F is Finite_Sep_Sequence of S holds ex G being Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds F . n = G . n ) & ( for m being Nat st not m in dom F holds G . m = {} ) ) let S be SigmaField of X; ::_thesis: for F being Function st F is Finite_Sep_Sequence of S holds ex G being Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds F . n = G . n ) & ( for m being Nat st not m in dom F holds G . m = {} ) ) let F be Function; ::_thesis: ( F is Finite_Sep_Sequence of S implies ex G being Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds F . n = G . n ) & ( for m being Nat st not m in dom F holds G . m = {} ) ) ) defpred S1[ set , set ] means ( ( $1 in dom F implies F . $1 = $2 ) & ( not $1 in dom F implies $2 = {} ) ); assume A1: F is Finite_Sep_Sequence of S ; ::_thesis: ex G being Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds F . n = G . n ) & ( for m being Nat st not m in dom F holds G . m = {} ) ) A2: for x1 being set st x1 in NAT holds ex y1 being set st ( y1 in S & S1[x1,y1] ) proof let x1 be set ; ::_thesis: ( x1 in NAT implies ex y1 being set st ( y1 in S & S1[x1,y1] ) ) assume x1 in NAT ; ::_thesis: ex y1 being set st ( y1 in S & S1[x1,y1] ) then reconsider x1 = x1 as Element of NAT ; percases ( x1 in dom F or not x1 in dom F ) ; supposeA3: x1 in dom F ; ::_thesis: ex y1 being set st ( y1 in S & S1[x1,y1] ) then A4: F . x1 in rng F by FUNCT_1:def_3; A5: rng F c= S by A1, FINSEQ_1:def_4; take F . x1 ; ::_thesis: ( F . x1 in S & S1[x1,F . x1] ) thus ( F . x1 in S & S1[x1,F . x1] ) by A3, A4, A5; ::_thesis: verum end; supposeA6: not x1 in dom F ; ::_thesis: ex y1 being set st ( y1 in S & S1[x1,y1] ) take {} ; ::_thesis: ( {} in S & S1[x1, {} ] ) thus ( {} in S & S1[x1, {} ] ) by A6, PROB_1:4; ::_thesis: verum end; end; end; consider G being Function of NAT,S such that A7: for x1 being set st x1 in NAT holds S1[x1,G . x1] from FUNCT_2:sch_1(A2); for n, m being set st n <> m holds G . n misses G . m proof let n, m be set ; ::_thesis: ( n <> m implies G . n misses G . m ) assume A8: n <> m ; ::_thesis: G . n misses G . m percases ( ( n in NAT & m in NAT ) or not n in NAT or not m in NAT ) ; supposeA9: ( n in NAT & m in NAT ) ; ::_thesis: G . n misses G . m now__::_thesis:_G_._n_misses_G_._m percases ( ( n in dom F & m in dom F ) or not n in dom F or not m in dom F ) ; suppose ( n in dom F & m in dom F ) ; ::_thesis: G . n misses G . m then ( G . n = F . n & G . m = F . m ) by A7, A9; hence G . n misses G . m by A1, A8, PROB_2:def_2; ::_thesis: verum end; supposeA10: ( not n in dom F or not m in dom F ) ; ::_thesis: G . n misses G . m now__::_thesis:_G_._n_misses_G_._m percases ( not n in dom F or not m in dom F ) by A10; suppose not n in dom F ; ::_thesis: G . n misses G . m then G . n = {} by A7, A9; hence G . n misses G . m by XBOOLE_1:65; ::_thesis: verum end; suppose not m in dom F ; ::_thesis: G . n misses G . m then G . m = {} by A7, A9; hence G . n misses G . m by XBOOLE_1:65; ::_thesis: verum end; end; end; hence G . n misses G . m ; ::_thesis: verum end; end; end; hence G . n misses G . m ; ::_thesis: verum end; suppose ( not n in NAT or not m in NAT ) ; ::_thesis: G . n misses G . m then ( not n in dom G or not m in dom G ) ; then ( G . n = {} or G . m = {} ) by FUNCT_1:def_2; hence G . n misses G . m by XBOOLE_1:65; ::_thesis: verum end; end; end; then reconsider G = G as Sep_Sequence of S by PROB_2:def_2; take G ; ::_thesis: ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds F . n = G . n ) & ( for m being Nat st not m in dom F holds G . m = {} ) ) for x1 being set st x1 in union (rng F) holds x1 in union (rng G) proof let x1 be set ; ::_thesis: ( x1 in union (rng F) implies x1 in union (rng G) ) assume x1 in union (rng F) ; ::_thesis: x1 in union (rng G) then consider Y being set such that A11: x1 in Y and A12: Y in rng F by TARSKI:def_4; consider k being set such that A13: k in dom F and A14: Y = F . k by A12, FUNCT_1:def_3; dom F c= NAT by A1, RELAT_1:def_18; then reconsider k = k as Element of NAT by A13; A15: F . k = G . k by A7, A13; G . k in rng G by FUNCT_2:4; hence x1 in union (rng G) by A11, A14, A15, TARSKI:def_4; ::_thesis: verum end; then A16: union (rng F) c= union (rng G) by TARSKI:def_3; for x1 being set st x1 in union (rng G) holds x1 in union (rng F) proof let x1 be set ; ::_thesis: ( x1 in union (rng G) implies x1 in union (rng F) ) assume x1 in union (rng G) ; ::_thesis: x1 in union (rng F) then consider Y being set such that A17: x1 in Y and A18: Y in rng G by TARSKI:def_4; consider k being set such that A19: k in dom G and A20: Y = G . k by A18, FUNCT_1:def_3; reconsider k = k as Element of NAT by A19; A21: k in dom F by A7, A17, A20; A22: F . k = G . k by A7, A17, A20; F . k in rng F by A21, FUNCT_1:def_3; hence x1 in union (rng F) by A17, A20, A22, TARSKI:def_4; ::_thesis: verum end; then union (rng G) c= union (rng F) by TARSKI:def_3; hence union (rng F) = union (rng G) by A16, XBOOLE_0:def_10; ::_thesis: ( ( for n being Nat st n in dom F holds F . n = G . n ) & ( for m being Nat st not m in dom F holds G . m = {} ) ) hereby ::_thesis: for m being Nat st not m in dom F holds G . m = {} let n be Nat; ::_thesis: ( n in dom F implies F . n = G . n ) n in NAT by ORDINAL1:def_12; hence ( n in dom F implies F . n = G . n ) by A7; ::_thesis: verum end; let m be Nat; ::_thesis: ( not m in dom F implies G . m = {} ) m in NAT by ORDINAL1:def_12; hence ( not m in dom F implies G . m = {} ) by A7; ::_thesis: verum end; theorem :: MESFUNC2:31 for X being non empty set for S being SigmaField of X for F being Function st F is Finite_Sep_Sequence of S holds union (rng F) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for F being Function st F is Finite_Sep_Sequence of S holds union (rng F) in S let S be SigmaField of X; ::_thesis: for F being Function st F is Finite_Sep_Sequence of S holds union (rng F) in S let F be Function; ::_thesis: ( F is Finite_Sep_Sequence of S implies union (rng F) in S ) assume F is Finite_Sep_Sequence of S ; ::_thesis: union (rng F) in S then ex G being Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds F . n = G . n ) & ( for m being Nat st not m in dom F holds G . m = {} ) ) by Th30; hence union (rng F) in S ; ::_thesis: verum end; definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,ExtREAL; predf is_simple_func_in S means :Def4: :: MESFUNC2:def 4 ( f is V75() & ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( 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 ) ) ); end; :: deftheorem Def4 defines is_simple_func_in MESFUNC2:def_4_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL holds ( f is_simple_func_in S iff ( f is V75() & ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( 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 ) ) ) ); theorem :: MESFUNC2:32 for X being non empty set for f being PartFunc of X,ExtREAL st f is V75() holds rng f is Subset of REAL proof let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL st f is V75() holds rng f is Subset of REAL let f be PartFunc of X,ExtREAL; ::_thesis: ( f is V75() implies rng f is Subset of REAL ) assume A1: f is V75() ; ::_thesis: rng f is Subset of REAL rng f c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in REAL ) assume A2: y in rng f ; ::_thesis: y in REAL then reconsider y = y as R_eal ; consider x being set such that A3: x in dom f and A4: y = f . x by A2, FUNCT_1:def_3; reconsider x = x as Element of X by A3; A5: |.(f . x).| < +infty by A1, A3, Def1; then - +infty < y by A4, EXTREAL2:10; then A6: -infty < y by XXREAL_3:def_3; y < +infty by A4, A5, EXTREAL2:10; hence y in REAL by A6, XXREAL_0:14; ::_thesis: verum end; hence rng f is Subset of REAL ; ::_thesis: verum end; theorem :: MESFUNC2:33 for X being non empty set for S being SigmaField of X for n being Nat for F being Relation st F is Finite_Sep_Sequence of S holds F | (Seg n) is Finite_Sep_Sequence of S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for n being Nat for F being Relation st F is Finite_Sep_Sequence of S holds F | (Seg n) is Finite_Sep_Sequence of S let S be SigmaField of X; ::_thesis: for n being Nat for F being Relation st F is Finite_Sep_Sequence of S holds F | (Seg n) is Finite_Sep_Sequence of S let n be Nat; ::_thesis: for F being Relation st F is Finite_Sep_Sequence of S holds F | (Seg n) is Finite_Sep_Sequence of S let F be Relation; ::_thesis: ( F is Finite_Sep_Sequence of S implies F | (Seg n) is Finite_Sep_Sequence of S ) assume A1: F is Finite_Sep_Sequence of S ; ::_thesis: F | (Seg n) is Finite_Sep_Sequence of S then reconsider G = F | (Seg n) as FinSequence of S by FINSEQ_1:18; reconsider F = F as FinSequence of S by A1; for k, m being set st k <> m holds G . k misses G . m proof let k, m be set ; ::_thesis: ( k <> m implies G . k misses G . m ) assume A2: k <> m ; ::_thesis: G . k misses G . m percases ( ( k in dom G & m in dom G ) or not k in dom G or not m in dom G ) ; suppose ( k in dom G & m in dom G ) ; ::_thesis: G . k misses G . m then ( G . k = F . k & G . m = F . m ) by FUNCT_1:47; hence G . k misses G . m by A1, A2, PROB_2:def_2; ::_thesis: verum end; suppose ( not k in dom G or not m in dom G ) ; ::_thesis: G . k misses G . m then ( G . k = {} or G . m = {} ) by FUNCT_1:def_2; hence G . k misses G . m by XBOOLE_1:65; ::_thesis: verum end; end; end; hence F | (Seg n) is Finite_Sep_Sequence of S by PROB_2:def_2; ::_thesis: verum end; theorem :: MESFUNC2:34 for X being non empty set 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 proof 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 Def4; reconsider F = F as FinSequence of S ; defpred S1[ Nat] means ( $1 <= len F implies f | (union (rng (F | (Seg $1)))) is_measurable_on A ); A4: S1[ 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: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 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_11; 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:4; ::_thesis: verum end; hence f | (union (rng (F | (Seg 0)))) is_measurable_on A by MESFUNC1:def_16; ::_thesis: verum end; A7: for m being Nat st S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A8: ( m <= len F implies f | (union (rng (F | (Seg m)))) is_measurable_on A ) ; ::_thesis: S1[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_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__::_thesis:_A_/\_(less_dom_((f_|_(union_(rng_(F_|_(Seg_(m_+_1)))))),(R_EAL_r)))_in_S percases ( F . (m + 1) = {} or F . (m + 1) <> {} ) ; supposeA11: 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: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_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_16, XXREAL_0:2; ::_thesis: verum end; supposeA12: 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: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 V75() by A1, Def4; then A18: |.(f . x).| < +infty by A17, Def1; then - +infty < f . x by EXTREAL2:10; then A19: -infty < f . x by XXREAL_3:def_3; f . x < +infty by A18, EXTREAL2:10; then reconsider r1 = f . x as Real by A19, XXREAL_0:14; now__::_thesis:_A_/\_(less_dom_((f_|_(union_(rng_(F_|_(Seg_(m_+_1)))))),(R_EAL_r)))_in_S percases ( r <= r1 or r1 < r ) ; supposeA20: r <= r1 ; ::_thesis: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S 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 A21: 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 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_EAL 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: 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 A26: x1 in dom (f | (union (rng G1))) by A23, RELAT_1:61; 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_EAL r)) by A24, A26, MESFUNC1:def_11; ::_thesis: verum end; then A27: 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 A28: 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 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_EAL 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_EAL r)) by A33, A34, MESFUNC1:def_11; ::_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; then less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) = less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) by A27, XBOOLE_0:def_10; hence A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S by A8, A9, A10, MESFUNC1:def_16, XXREAL_0:2; ::_thesis: verum end; supposeA35: r1 < r ; ::_thesis: A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) in S 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 A36: 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 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_EAL_r)))_\/_(F_._(m_+_1)) percases ( x1 in (dom f) /\ (union (rng G1)) or x1 in (dom f) /\ (F . (m + 1)) ) by A38, XBOOLE_0:def_3; supposeA39: 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 ; 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_EAL 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_EAL r)) by A40, A42, MESFUNC1:def_11; 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 A43: 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 A44: 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__::_thesis:_x1_in_less_dom_((f_|_(union_(rng_(F_|_(Seg_(m_+_1)))))),(R_EAL_r)) percases ( x1 in less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) or x1 in F . (m + 1) ) by A44, XBOOLE_0:def_3; supposeA45: 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 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_EAL 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_EAL r)) by A50, A51, MESFUNC1:def_11; ::_thesis: verum end; supposeA52: x1 in F . (m + 1) ; ::_thesis: x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL 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 = 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:47; hence x1 in less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) by A35, A55, A56, MESFUNC1:def_11; ::_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; 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_16, 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: 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_16; ::_thesis: verum end; hence S1[m + 1] ; ::_thesis: verum end; A58: for n being Nat holds S1[n] from NAT_1:sch_2(A4, A7); F | (Seg (len F)) = F by FINSEQ_3:49; then f | (dom f) is_measurable_on A by A2, A58; hence f is_measurable_on A by RELAT_1:68; ::_thesis: verum end;