mesfunc2.miz



    begin

    reserve X for non empty set;

    reserve e for set;

    reserve x for Element of X;

    reserve f,g for PartFunc of X, ExtREAL ;

    reserve S for SigmaField of X;

    reserve F for Function of RAT , S;

    reserve p,q for Rational;

    reserve r for Real;

    reserve n,m for Nat;

    reserve A,B for Element of S;

    definition

      let X, f;

      :: original: real-valued

      redefine

      :: MESFUNC2:def1

      attr f is real-valued means for x st x in ( dom f) holds |.(f . x).| < +infty ;

      compatibility

      proof

        thus f is real-valued implies for x st x in ( dom f) holds |.(f . x).| < +infty

        proof

          assume

           A1: f is real-valued;

          let x;

          assume x in ( dom f);

          then

           A2: (f . x) in ( rng f) by FUNCT_1: 3;

          ( rng f) c= REAL by A1;

          hence thesis by A2, EXTREAL1: 41;

        end;

        assume

         A3: for x st x in ( dom f) holds |.(f . x).| < +infty ;

        let e be object;

        assume

         A4: e in ( dom f);

        then

        reconsider x = e as Element of X;

         |.(f . x).| < +infty by A3, A4;

        then (f . x) in REAL by EXTREAL1: 41;

        hence thesis;

      end;

    end

    theorem :: MESFUNC2:1

    f = (1 (#) f)

    proof

      

       A1: ( dom f) = ( dom (1 (#) f)) by MESFUNC1:def 6;

      for x st x in ( dom (1 (#) f)) holds (f . x) = ((1 (#) f) . x)

      proof

        let x;

        assume x in ( dom (1 (#) f));

        then ((1 (#) f) . x) = (1 * (f . x)) by MESFUNC1:def 6;

        hence thesis by XXREAL_3: 81;

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: MESFUNC2:2

    

     Th2: f is real-valued or g is real-valued implies ( dom (f + g)) = (( dom f) /\ ( dom g)) & ( dom (f - g)) = (( dom f) /\ ( dom g))

    proof

      assume

       A1: f is real-valued or g is real-valued;

      now

        per cases by A1;

          suppose

           A2: f is real-valued;

          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 thesis by A6, MESFUNC1:def 4;

        end;

          suppose

           A7: g is real-valued;

          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 thesis by A11, MESFUNC1:def 4;

        end;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC2:3

    

     Th3: for f, g, F, r, A st f is real-valued & g is real-valued & (for p holds (F . p) = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p)))))) holds (A /\ ( less_dom ((f + g),r))) = ( union ( rng F))

    proof

      let f, g, F, r, A;

      assume that

       A1: f is real-valued and

       A2: g is real-valued and

       A3: for p holds (F . p) = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p)))));

      

       A4: ( dom (f + g)) = (( dom f) /\ ( dom g)) by A1, Th2;

      

       A5: (A /\ ( less_dom ((f + g),r))) c= ( union ( rng F))

      proof

        let x be object;

        assume

         A6: x in (A /\ ( less_dom ((f + g),r)));

        then

         A7: x in A by XBOOLE_0:def 4;

        

         A8: x in ( less_dom ((f + g),r)) by A6, XBOOLE_0:def 4;

        then

         A9: x in ( dom (f + g)) by MESFUNC1:def 11;

        

         A10: ((f + g) . x) < r by A8, MESFUNC1:def 11;

        reconsider x as Element of X by A6;

        

         A11: ((f . x) + (g . x)) < 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;

        

         A15: |.(g . x).| < +infty by A2, A13;

        

         A16: ( - +infty ) < (f . x) by A14, EXTREAL1: 21;

        

         A17: (f . x) < +infty by A14, EXTREAL1: 21;

        

         A18: ( - +infty ) < (g . x) by A15, EXTREAL1: 21;

        

         A19: (g . x) < +infty by A15, EXTREAL1: 21;

        then

         A20: (f . x) < (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 Element of REAL by A17, A21, XXREAL_0: 14;

        reconsider g1 = (g . x) as Element of REAL by A19, A22, XXREAL_0: 14;

        reconsider rr = r as R_eal by XXREAL_0:def 1;

        f1 < (r - g1) by A20, SUPINF_2: 3;

        then

        consider p such that

         A23: f1 < p and

         A24: p < (r - g1) by RAT_1: 7;

        

         A25: not (r - p) <= g1 by A24, XREAL_1: 12;

        

         A26: x in ( less_dom (f,p)) by A12, A23, MESFUNC1:def 11;

        

         A27: x in ( less_dom (g,(r - p))) by A13, A25, MESFUNC1:def 11;

        

         A28: x in (A /\ ( less_dom (f,p))) by A7, A26, XBOOLE_0:def 4;

        x in (A /\ ( less_dom (g,(r - p)))) by A7, A27, XBOOLE_0:def 4;

        then

         A29: x in ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(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 thesis by A31, TARSKI:def 4;

      end;

      ( union ( rng F)) c= (A /\ ( less_dom ((f + g),r)))

      proof

        let x be object;

        assume x in ( union ( rng F));

        then

        consider Y be set such that

         A32: x in Y and

         A33: Y in ( rng F) by TARSKI:def 4;

        consider p be object such that

         A34: p in ( dom F) and

         A35: Y = (F . p) by A33, FUNCT_1:def 3;

        reconsider p as Rational by A34;

        

         A36: x in ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p))))) by A3, A32, A35;

        then

         A37: x in (A /\ ( less_dom (f,p))) by XBOOLE_0:def 4;

        

         A38: x in (A /\ ( less_dom (g,(r - p)))) by A36, XBOOLE_0:def 4;

        

         A39: x in A by A37, XBOOLE_0:def 4;

        

         A40: x in ( less_dom (f,p)) by A37, XBOOLE_0:def 4;

        

         A41: x in ( less_dom (g,(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 as Element of X by A36;

        

         A44: (g . x) < (r - p) by A41, MESFUNC1:def 11;

        

         A45: |.(f . x).| < +infty by A1, A42;

        

         A46: |.(g . x).| < +infty by A2, A43;

        

         A47: ( - +infty ) < (f . x) by A45, EXTREAL1: 21;

        

         A48: ( - +infty ) < (g . x) by A46, EXTREAL1: 21;

        

         A49: -infty < (f . x) by A47, XXREAL_3: 23;

        

         A50: (f . x) < +infty by A45, EXTREAL1: 21;

        

         A51: -infty < (g . x) by A48, XXREAL_3: 23;

        

         A52: (g . x) < +infty by A46, EXTREAL1: 21;

        reconsider f1 = (f . x) as Element of REAL by A49, A50, XXREAL_0: 14;

        reconsider g1 = (g . x) as Element of 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)) by A54, A55, MESFUNC1:def 11;

        hence thesis by A39, XBOOLE_0:def 4;

      end;

      hence thesis by A5;

    end;

    begin

    theorem :: MESFUNC2:4

    ex F be sequence of RAT st F is one-to-one & ( dom F) = NAT & ( rng F) = RAT

    proof

      consider F be 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 sequence of RAT by A2, FUNCT_2: 2;

      hence thesis by A1, A2;

    end;

    theorem :: MESFUNC2:5

    

     Th5: for X,Y,Z be non empty set, F be Function of X, Z st (X,Y) are_equipotent holds ex G be Function of Y, Z st ( rng F) = ( rng G)

    proof

      let X,Y,Z be non empty set;

      let F be Function of X, Z;

      assume (X,Y) are_equipotent ;

      then

      consider H be 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 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 be Element of Z holds z in ( rng F) implies z in ( rng G)

      proof

        let z be Element of Z;

        assume z in ( rng F);

        then

        consider x be object 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 thesis by A1, A3, A6, A7, FUNCT_1: 35;

      end;

      then

       A9: ( rng F) c= ( rng G);

      for z be Element of Z holds z in ( rng G) implies z in ( rng F)

      proof

        let z be Element of Z;

        assume z in ( rng G);

        then

        consider y be object 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 be object 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 thesis by A10, A11, A15, FUNCT_1: 12;

      end;

      then ( rng G) c= ( rng F);

      then ( rng F) = ( rng G) by A9;

      hence thesis;

    end;

    theorem :: MESFUNC2:6

    

     Th6: for S, f, g, A st f is A -measurable & g is A -measurable holds ex F be Function of RAT , S st for p be Rational holds (F . p) = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p)))))

    proof

      let S, f, g, A;

      assume

       A1: f is A -measurable & g is A -measurable;

      defpred P[ object, object] means ex p st p = $1 & $2 = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p)))));

      

       A2: for x1 be object st x1 in RAT holds ex y1 be object st y1 in S & P[x1, y1]

      proof

        let x1 be object;

        assume x1 in RAT ;

        then

        consider p such that

         A3: p = x1;

        

         A4: (A /\ ( less_dom (f,p))) in S & (A /\ ( less_dom (g,(r - p)))) in S by A1;

        take ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p)))));

        thus thesis by A3, A4, FINSUB_1:def 2;

      end;

      consider G be Function of RAT , S such that

       A5: for x1 be object st x1 in RAT holds P[x1, (G . x1)] from FUNCT_2:sch 1( A2);

      

       A6: for p be Rational holds (G . p) = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p)))))

      proof

        let p be Rational;

        p in RAT by RAT_1:def 2;

        then ex q st q = p & (G . p) = ((A /\ ( less_dom (f,q))) /\ (A /\ ( less_dom (g,(r - q))))) by A5;

        hence thesis;

      end;

      take G;

      thus thesis by A6;

    end;

    theorem :: MESFUNC2:7

    

     Th7: for f, g, A st f is real-valued & g is real-valued & f is A -measurable & g is A -measurable holds (f + g) is A -measurable

    proof

      let f, g, A;

      assume that

       A1: f is real-valued & g is real-valued and

       A2: f is A -measurable & g is A -measurable;

      for r be Real holds (A /\ ( less_dom ((f + g),r))) in S

      proof

        let r be Real;

        reconsider r as Real;

        consider F be Function of RAT , S such that

         A3: for p be Rational holds (F . p) = ((A /\ ( less_dom (f,p))) /\ (A /\ ( less_dom (g,(r - p))))) by A2, Th6;

        consider G be sequence of S such that

         A4: ( rng F) = ( rng G) by Th5, MESFUNC1: 5;

        (A /\ ( less_dom ((f + g),r))) = ( union ( rng G)) by A1, A3, A4, Th3;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC2:8

    

     Th8: for C be non empty set, f1,f2 be PartFunc of C, ExtREAL holds (f1 - f2) = (f1 + ( - f2))

    proof

      let C be non empty set;

      let f1,f2 be PartFunc of C, ExtREAL ;

      

       A1: ( dom (f1 - f2)) = ((( dom f1) /\ ( dom f2)) \ (((f1 " { +infty }) /\ (f2 " { +infty })) \/ ((f1 " { -infty }) /\ (f2 " { -infty })))) by MESFUNC1:def 4;

      for x be Element of C st x in (f2 " { +infty }) holds x in (( - f2) " { -infty })

      proof

        let x be Element of C;

        assume

         A2: 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 thesis by A5, FUNCT_1:def 7;

      end;

      then

       A6: (f2 " { +infty }) c= (( - f2) " { -infty });

      for x be Element of C st x in (( - f2) " { -infty }) holds x in (f2 " { +infty })

      proof

        let x be Element of C;

        assume

         A7: 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 thesis by A10, FUNCT_1:def 7;

      end;

      then (( - f2) " { -infty }) c= (f2 " { +infty });

      then

       A11: (f2 " { +infty }) = (( - f2) " { -infty }) by A6;

      for x be Element of C st x in (f2 " { -infty }) holds x in (( - f2) " { +infty })

      proof

        let x be Element of C;

        assume

         A12: 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 thesis by A15, FUNCT_1:def 7;

      end;

      then

       A16: (f2 " { -infty }) c= (( - f2) " { +infty });

      for x be Element of C st x in (( - f2) " { +infty }) holds x in (f2 " { -infty })

      proof

        let x be Element of C;

        assume

         A17: 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 thesis by A20, FUNCT_1:def 7;

      end;

      then (( - f2) " { +infty }) c= (f2 " { -infty });

      then

       A21: (f2 " { -infty }) = (( - f2) " { +infty }) by A16;

      ( 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 be Element of C st x in ( dom (f1 - f2)) holds ((f1 - f2) . x) = ((f1 + ( - f2)) . x)

      proof

        let x be Element of C;

        assume

         A23: x in ( dom (f1 - f2));

        ( 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 thesis by A24, MESFUNC1:def 7;

      end;

      hence thesis by A22, PARTFUN1: 5;

    end;

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    theorem :: MESFUNC2:9

    

     Th9: for C be non empty set, f be PartFunc of C, ExtREAL holds ( - f) = (( - 1) (#) f)

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      

       A1: ( dom ( - f)) = ( dom f) by MESFUNC1:def 7;

      

       A2: ( dom (( - 1) (#) f)) = ( dom f) by MESFUNC1:def 6;

      for x be Element of C st x in ( dom f) holds (( - f) . x) = ((( - 1) (#) f) . x)

      proof

        let x be Element of C;

        assume

         A3: x in ( dom f);

        then

         A4: ((( - 1) (#) f) . x) = (( - 1) * (f . x)) by A2, MESFUNC1:def 6;

        ((( - 1) (#) f) . x) = ((( - jj) (#) f) . x)

        .= (( - 1. ) * (f . x)) by SUPINF_2: 2, A4

        .= ( - ( 1. * (f . x))) by XXREAL_3: 92

        .= ( - (1 * (f . x)))

        .= ( - (f . x)) by XXREAL_3: 81;

        hence thesis by A1, A3, MESFUNC1:def 7;

      end;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: MESFUNC2:10

    

     Th10: for C be non empty set, f be PartFunc of C, ExtREAL , r be Real st f is real-valued holds (r (#) f) is real-valued

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let r be Real;

      assume

       A1: f is real-valued;

      for x be Element of C st x in ( dom (r (#) f)) holds |.((r (#) f) . x).| < +infty

      proof

        let x be Element of C;

        assume

         A2: x in ( dom (r (#) f));

        then x in ( dom f) by MESFUNC1:def 6;

        then

         A3: |.(f . x).| < +infty by A1;

        then ( - +infty ) < (f . x) by EXTREAL1: 21;

        then

         A4: -infty < (f . x) by XXREAL_3:def 3;

        (f . x) < +infty by A3, EXTREAL1: 21;

        then

        reconsider y = (f . x) as Element of REAL by A4, XXREAL_0: 14;

        reconsider yy = (f . x) as Element of ExtREAL ;

        reconsider ry = (r * y) as Element of REAL by XREAL_0:def 1;

        

         A5: -infty < ry by XXREAL_0: 12;

        

         A6: ry < +infty by XXREAL_0: 9;

        

         A7: -infty < (r * y) by A5;

        

         A8: (r * y) = (r * yy) by XXREAL_3:def 5

        .= ((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;

        hence thesis by A9, EXTREAL1: 22;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC2:11

    for f, g, A st f is real-valued & g is real-valued & f is A -measurable & g is A -measurable & A c= ( dom g) holds (f - g) is A -measurable

    proof

      let f, g, A;

      assume that

       A1: f is real-valued and

       A2: g is real-valued and

       A3: f is A -measurable and

       A4: g is A -measurable & A c= ( dom g);

      

       A5: (( - 1) (#) g) is real-valued by A2, Th10;

      

       A6: (( - 1) (#) g) is A -measurable by A4, MESFUNC1: 37;

      

       A7: ( - g) is real-valued by A5, Th9;

      ( - g) is A -measurable by A6, Th9;

      then (f + ( - g)) is A -measurable by A1, A3, A7, Th7;

      hence thesis by Th8;

    end;

    begin

    definition

      let C be non empty set, f be PartFunc of C, ExtREAL ;

      deffunc F( Element of C) = ( max ((f . $1), 0. ));

      :: MESFUNC2:def2

      func max+ (f) -> PartFunc of C, ExtREAL means

      : Def2: ( dom it ) = ( dom f) & for x be Element of C st x in ( dom it ) holds (it . x) = ( max ((f . x), 0. ));

      existence

      proof

        defpred P[ Element of C] means $1 in ( dom f);

        consider F be PartFunc of C, ExtREAL such that

         A1: for c be Element of C holds c in ( dom F) iff P[c] and

         A2: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        thus ( dom F) = ( dom f)

        proof

          thus ( dom F) c= ( dom f) by A1;

          let x be object;

          assume x in ( dom f);

          hence thesis by A1;

        end;

        let c be Element of C;

        assume c in ( dom F);

        hence thesis by A2;

      end;

      uniqueness

      proof

        set X = ( dom f);

        thus for F,G be PartFunc of C, ExtREAL st (( dom F) = X & for c be Element of C st c in ( dom F) holds (F . c) = F(c)) & (( dom G) = X & for c be Element of C st c in ( dom G) holds (G . c) = F(c)) holds F = G from SEQ_1:sch 4;

      end;

      deffunc F( Element of C) = ( max (( - (f . $1)), 0. ));

      :: MESFUNC2:def3

      func max- (f) -> PartFunc of C, ExtREAL means

      : Def3: ( dom it ) = ( dom f) & for x be Element of C st x in ( dom it ) holds (it . x) = ( max (( - (f . x)), 0. ));

      existence

      proof

        defpred P[ Element of C] means $1 in ( dom f);

        consider F be PartFunc of C, ExtREAL such that

         A3: for c be Element of C holds c in ( dom F) iff P[c] and

         A4: for c be Element of C st c in ( dom F) holds (F . c) = F(c) from SEQ_1:sch 3;

        take F;

        thus ( dom F) = ( dom f)

        proof

          thus ( dom F) c= ( dom f) by A3;

          let x be object;

          assume x in ( dom f);

          hence thesis by A3;

        end;

        let c be Element of C;

        assume c in ( dom F);

        hence thesis by A4;

      end;

      uniqueness

      proof

        set X = ( dom f);

        thus for F,G be PartFunc of C, ExtREAL st (( dom F) = X & for c be Element of C st c in ( dom F) holds (F . c) = F(c)) & (( dom G) = X & for c be Element of C st c in ( dom G) holds (G . c) = F(c)) holds F = G from SEQ_1:sch 4;

      end;

    end

    theorem :: MESFUNC2:12

    

     Th12: for C be non empty set, f be PartFunc of C, ExtREAL , x be Element of C holds 0. <= (( max+ f) . x)

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      

       A1: ( dom ( max+ f)) = ( dom f) by Def2;

      per cases ;

        suppose x in ( dom f);

        then (( max+ f) . x) = ( max ((f . x), 0. )) by A1, Def2;

        hence thesis by XXREAL_0: 25;

      end;

        suppose not x in ( dom f);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: MESFUNC2:13

    

     Th13: for C be non empty set, f be PartFunc of C, ExtREAL , x be Element of C holds 0. <= (( max- f) . x)

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      

       A1: ( dom ( max- f)) = ( dom f) by Def3;

      per cases ;

        suppose x in ( dom f);

        then (( max- f) . x) = ( max (( - (f . x)), 0. )) by A1, Def3;

        hence thesis by XXREAL_0: 25;

      end;

        suppose not x in ( dom f);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: MESFUNC2:14

    for C be non empty set, f be PartFunc of C, ExtREAL holds ( max- f) = ( max+ ( - f))

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      

       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 be Element of C st x in ( dom ( max- f)) holds (( max- f) . x) = (( max+ ( - f)) . x)

      proof

        let x be Element of C;

        assume

         A3: x in ( dom ( max- f));

        then (( max- f) . x) = ( max (( - (f . x)), 0. )) & ( - (f . x)) = (( - f) . x) by A1, Def3, MESFUNC1:def 7;

        hence thesis by A2, A3, Def2;

      end;

      hence thesis by A2, PARTFUN1: 5;

    end;

    theorem :: MESFUNC2:15

    

     Th15: for C be non empty set, f be PartFunc of C, ExtREAL , x be Element of C st 0. < (( max+ f) . x) holds (( max- f) . x) = 0.

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      

       A1: ( dom ( max+ f)) = ( dom f) by Def2;

      per cases ;

        suppose

         A2: x in ( dom f);

        assume

         A3: 0. < (( max+ f) . x);

        

         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. & 0. <= 0. ) by A3, XXREAL_0: 28;

        then ( max (( - (f . x)), 0. )) = 0. by XXREAL_0:def 10;

        hence thesis by A5, Def3;

      end;

        suppose not x in ( dom f);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: MESFUNC2:16

    for C be non empty set, f be PartFunc of C, ExtREAL , x be Element of C st 0. < (( max- f) . x) holds (( max+ f) . x) = 0.

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      

       A1: ( dom ( max- f)) = ( dom f) by Def3;

      per cases ;

        suppose

         A2: x in ( dom f);

        assume

         A3: 0. < (( max- f) . x);

        

         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 thesis by A5, Def2;

      end;

        suppose not x in ( dom f);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: MESFUNC2:17

    

     Th17: for C be non empty set, f be 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;

      let f be PartFunc of C, ExtREAL ;

      

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

        then

        consider x1 be object such that

         A2: x1 in (( max+ f) " { +infty }) and

         A3: x1 in (( max- f) " { +infty }) by XBOOLE_0: 3;

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

      end;

      then

       A7: ((( max+ f) " { +infty }) /\ (( max- f) " { +infty })) = {} ;

      (( max+ f) " { -infty }) misses (( max- f) " { -infty })

      proof

        assume not (( max+ f) " { -infty }) misses (( max- f) " { -infty });

        then

        consider x1 be object such that

         A8: x1 in (( max+ f) " { -infty }) and x1 in (( max- f) " { -infty }) by XBOOLE_0: 3;

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

      end;

      then

       A9: ((( max+ f) " { -infty }) /\ (( max- f) " { -infty })) = {} ;

      (( max+ f) " { +infty }) misses (( max- f) " { -infty })

      proof

        assume not (( max+ f) " { +infty }) misses (( max- f) " { -infty });

        then

        consider x1 be object such that

         A10: x1 in (( max+ f) " { +infty }) and

         A11: x1 in (( max- f) " { -infty }) by XBOOLE_0: 3;

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

      end;

      then

       A12: ((( max+ f) " { +infty }) /\ (( max- f) " { -infty })) = {} ;

      (( max+ f) " { -infty }) misses (( max- f) " { +infty })

      proof

        assume not (( max+ f) " { -infty }) misses (( max- f) " { +infty });

        then

        consider x1 be object such that

         A13: x1 in (( max+ f) " { -infty }) and x1 in (( max- f) " { +infty }) by XBOOLE_0: 3;

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

      end;

      then

       A14: ((( max+ f) " { -infty }) /\ (( max- f) " { +infty })) = {} ;

      ( dom (( max+ f) - ( max- f))) = ((( dom f) /\ ( dom f)) \ ( {} \/ {} )) by A1, A7, A9, MESFUNC1:def 4;

      hence thesis by A1, A12, A14, MESFUNC1:def 3;

    end;

    theorem :: MESFUNC2:18

    

     Th18: for C be non empty set, f be PartFunc of C, ExtREAL , x be 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;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      

       A1: ( dom ( max- f)) = ( dom f) & ( dom ( max+ f)) = ( dom f) by Def2, Def3;

      per cases ;

        suppose

         A2: x in ( dom f);

        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 thesis by A5, XXREAL_0: 16;

      end;

        suppose not x in ( dom f);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: MESFUNC2:19

    

     Th19: for C be non empty set, f be PartFunc of C, ExtREAL , x be Element of C st (( max+ f) . x) = (f . x) holds (( max- f) . x) = 0.

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      

       A1: ( dom ( max- f)) = ( dom f) by Def3;

      per cases ;

        suppose

         A2: x in ( dom f);

        assume

         A3: (( max+ f) . x) = (f . x);

        

         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 thesis by A7, XXREAL_0:def 10;

      end;

        suppose not x in ( dom f);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: MESFUNC2:20

    

     Th20: for C be non empty set, f be PartFunc of C, ExtREAL , x be 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;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      assume that

       A1: x in ( dom f) and

       A2: (( max+ f) . x) = 0. ;

      

       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 thesis by A6, XXREAL_0:def 10;

    end;

    theorem :: MESFUNC2:21

    for C be non empty set, f be PartFunc of C, ExtREAL , x be Element of C st (( max- f) . x) = ( - (f . x)) holds (( max+ f) . x) = 0.

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      

       A1: ( dom ( max+ f)) = ( dom f) by Def2;

      per cases ;

        suppose

         A2: x in ( dom f);

        assume

         A3: (( max- f) . x) = ( - (f . x));

        

         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 thesis by A6, XXREAL_0:def 10;

      end;

        suppose not x in ( dom f);

        hence thesis by A1, FUNCT_1:def 2;

      end;

    end;

    theorem :: MESFUNC2:22

    for C be non empty set, f be PartFunc of C, ExtREAL , x be 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;

      let f be PartFunc of C, ExtREAL ;

      let x be Element of C;

      assume that

       A1: x in ( dom f) and

       A2: (( max- f) . x) = 0. ;

      

       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 thesis by A5, XXREAL_0:def 10;

    end;

    theorem :: MESFUNC2:23

    for C be non empty set, f be PartFunc of C, ExtREAL holds f = (( max+ f) - ( max- f))

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      

       A1: ( dom f) = ( dom (( max+ f) - ( max- f))) by Th17;

      for x be Element of C st x in ( dom f) holds (f . x) = ((( max+ f) - ( max- f)) . x)

      proof

        let x be Element of C;

        assume

         A2: x in ( dom f);

        then

         A3: ((( max+ f) - ( max- f)) . x) = ((( max+ f) . x) - (( max- f) . x)) by A1, MESFUNC1:def 4;

        per cases by Th18;

          suppose

           A4: (( max+ f) . x) = (f . x);

          then (( max- f) . x) = 0. by Th19;

          then ( - (( max- f) . x)) = 0 ;

          hence thesis by A3, A4, XXREAL_3: 4;

        end;

          suppose

           A5: (( max+ f) . x) = 0. ;

          then (( max- f) . x) = ( - (f . x)) by A2, Th20;

          hence thesis by A3, A5, XXREAL_3: 4;

        end;

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: MESFUNC2:24

    for C be non empty set, f be PartFunc of C, ExtREAL holds |.f.| = (( max+ f) + ( max- f))

    proof

      let C be non empty set;

      let f be PartFunc of C, ExtREAL ;

      

       A1: ( dom f) = ( dom (( max+ f) + ( max- f))) by Th17;

      

       A2: ( dom f) = ( dom |.f.|) by MESFUNC1:def 10;

      for x be Element of C st x in ( dom f) holds ( |.f.| . x) = ((( max+ f) + ( max- f)) . x)

      proof

        let x be Element of C;

        assume

         A3: x in ( dom f);

        now

          per cases by Th18;

            suppose

             A4: (( max+ f) . x) = (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 thesis by A1, A3, A5, MESFUNC1:def 3;

          end;

            suppose

             A6: (( max+ f) . x) = 0. ;

            

            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 EXTREAL1: 18

            .= ( |.f.| . x) by A2, A3, MESFUNC1:def 10;

            hence thesis by A1, A3, A7, MESFUNC1:def 3;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    begin

    theorem :: MESFUNC2:25

    f is A -measurable implies ( max+ f) is A -measurable

    proof

      assume

       A1: f is A -measurable;

      for r be Real holds (A /\ ( less_dom (( max+ f),r))) in S

      proof

        let r be Real;

        reconsider r as Real;

        now

          per cases ;

            suppose

             A2: 0 < r;

            for x be object st x in ( less_dom (( max+ f),r)) holds x in ( less_dom (f,r))

            proof

              let x be object;

              assume

               A3: x in ( less_dom (( max+ f),r));

              then

               A4: x in ( dom ( max+ f)) by MESFUNC1:def 11;

              

               A5: (( max+ f) . x) < r by A3, MESFUNC1:def 11;

              reconsider x as Element of X by A3;

              

               A6: ( max ((f . x), 0. )) < r by A4, A5, Def2;

              then

               A7: (f . x) <= r by XXREAL_0: 30;

              (f . x) <> r

              proof

                assume

                 A8: (f . x) = r;

                then ( max ((f . x), 0. )) = 0. by A6, XXREAL_0: 16;

                hence contradiction by A6, A8, XXREAL_0:def 10;

              end;

              then

               A9: (f . x) < r by A7, XXREAL_0: 1;

              x in ( dom f) by A4, Def2;

              hence thesis by A9, MESFUNC1:def 11;

            end;

            then

             A10: ( less_dom (( max+ f),r)) c= ( less_dom (f,r));

            for x be object st x in ( less_dom (f,r)) holds x in ( less_dom (( max+ f),r))

            proof

              let x be object;

              assume

               A11: x in ( less_dom (f,r));

              then

               A12: x in ( dom f) by MESFUNC1:def 11;

              

               A13: (f . x) < r by A11, MESFUNC1:def 11;

              reconsider x as Element of X by A11;

              

               A14: x in ( dom ( max+ f)) by A12, Def2;

              now

                per cases ;

                  suppose 0. <= (f . x);

                  then ( max ((f . x), 0. )) = (f . x) by XXREAL_0:def 10;

                  then (( max+ f) . x) = (f . x) by A14, Def2;

                  hence thesis by A13, A14, MESFUNC1:def 11;

                end;

                  suppose not 0. <= (f . x);

                  then ( max ((f . x), 0. )) = 0. by XXREAL_0:def 10;

                  then (( max+ f) . x) = 0. by A14, Def2;

                  hence thesis by A2, A14, MESFUNC1:def 11;

                end;

              end;

              hence thesis;

            end;

            then ( less_dom (f,r)) c= ( less_dom (( max+ f),r));

            then ( less_dom (( max+ f),r)) = ( less_dom (f,r)) by A10;

            hence thesis by A1;

          end;

            suppose

             A15: r <= 0 ;

            for x be Element of X holds not x in ( less_dom (( max+ f),r))

            proof

              let x be Element of X;

              assume

               A16: x in ( less_dom (( max+ f),r));

              then

               A17: x in ( dom ( max+ f)) by MESFUNC1:def 11;

              

               A18: (( max+ f) . x) < r by A16, MESFUNC1:def 11;

              (( max+ f) . x) = ( max ((f . x), 0. )) by A17, Def2;

              hence contradiction by A15, A18, XXREAL_0: 25;

            end;

            then ( less_dom (( max+ f),r)) = {} by SUBSET_1: 4;

            hence thesis by PROB_1: 4;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC2:26

    f is A -measurable & A c= ( dom f) implies ( max- f) is A -measurable

    proof

      assume

       A1: f is A -measurable & A c= ( dom f);

      for r be Real holds (A /\ ( less_dom (( max- f),r))) in S

      proof

        let r be Real;

        reconsider r as Real;

        now

          per cases ;

            suppose

             A2: 0 < r;

            (( - 1) (#) f) is A -measurable by A1, MESFUNC1: 37;

            then

             A3: ( - f) is A -measurable by Th9;

            for x be object st x in ( less_dom (( max- f),r)) holds x in ( less_dom (( - f),r))

            proof

              let x be object;

              assume

               A4: x in ( less_dom (( max- f),r));

              then

               A5: x in ( dom ( max- f)) by MESFUNC1:def 11;

              

               A6: (( max- f) . x) < r by A4, MESFUNC1:def 11;

              reconsider x as Element of X by A4;

              

               A7: ( max (( - (f . x)), 0. )) < r by A5, A6, Def3;

              then

               A8: ( - (f . x)) <= r by XXREAL_0: 30;

              ( - (f . x)) <> r

              proof

                assume

                 A9: ( - (f . x)) = r;

                then ( max (( - (f . x)), 0. )) = 0. by A7, XXREAL_0: 16;

                hence contradiction by A7, A9, XXREAL_0:def 10;

              end;

              then

               A10: ( - (f . x)) < 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 thesis by A10, A11, MESFUNC1:def 11;

            end;

            then

             A12: ( less_dom (( max- f),r)) c= ( less_dom (( - f),r));

            for x be object st x in ( less_dom (( - f),r)) holds x in ( less_dom (( max- f),r))

            proof

              let x be object;

              assume

               A13: x in ( less_dom (( - f),r));

              then

               A14: x in ( dom ( - f)) by MESFUNC1:def 11;

              

               A15: (( - f) . x) < r by A13, MESFUNC1:def 11;

              reconsider 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

                per cases ;

                  suppose 0. <= ( - (f . x));

                  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 thesis by A15, A16, MESFUNC1:def 11;

                end;

                  suppose not 0. <= ( - (f . x));

                  then ( max (( - (f . x)), 0. )) = 0. by XXREAL_0:def 10;

                  then (( max- f) . x) = 0. by A16, Def3;

                  hence thesis by A2, A16, MESFUNC1:def 11;

                end;

              end;

              hence thesis;

            end;

            then ( less_dom (( - f),r)) c= ( less_dom (( max- f),r));

            then ( less_dom (( max- f),r)) = ( less_dom (( - f),r)) by A12;

            hence thesis by A3;

          end;

            suppose

             A17: r <= 0 ;

            for x be Element of X holds not x in ( less_dom (( max- f),r))

            proof

              let x be Element of X;

              assume

               A18: x in ( less_dom (( max- f),r));

              then

               A19: x in ( dom ( max- f)) by MESFUNC1:def 11;

              

               A20: (( max- f) . x) < r by A18, MESFUNC1:def 11;

              (( max- f) . x) = ( max (( - (f . x)), 0. )) by A19, Def3;

              hence contradiction by A17, A20, XXREAL_0: 25;

            end;

            then ( less_dom (( max- f),r)) = {} by SUBSET_1: 4;

            hence thesis by PROB_1: 4;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC2:27

    for f, A st f is A -measurable & A c= ( dom f) holds |.f.| is A -measurable

    proof

      let f, A;

      assume

       A1: f is A -measurable & A c= ( dom f);

      for r be Real holds (A /\ ( less_dom ( |.f.|,r))) in S

      proof

        let r be Real;

        reconsider r as R_eal by XXREAL_0:def 1;

        for x be object st x in ( less_dom ( |.f.|,r)) holds x in (( less_dom (f,r)) /\ ( great_dom (f,( - r))))

        proof

          let x be object;

          assume

           A2: x in ( less_dom ( |.f.|,r));

          then

           A3: x in ( dom |.f.|) by MESFUNC1:def 11;

          

           A4: ( |.f.| . x) < r by A2, MESFUNC1:def 11;

          reconsider x as Element of X by A2;

          

           A5: x in ( dom f) by A3, MESFUNC1:def 10;

          

           A6: |.(f . x).| < r by A3, A4, MESFUNC1:def 10;

          then

           A7: ( - r) < (f . x) by EXTREAL1: 21;

          

           A8: (f . x) < r by A6, EXTREAL1: 21;

          

           A9: x in ( less_dom (f,r)) by A5, A8, MESFUNC1:def 11;

          x in ( great_dom (f,( - r))) by A5, A7, MESFUNC1:def 13;

          hence thesis by A9, XBOOLE_0:def 4;

        end;

        then

         A10: ( less_dom ( |.f.|,r)) c= (( less_dom (f,r)) /\ ( great_dom (f,( - r))));

        for x be object st x in (( less_dom (f,r)) /\ ( great_dom (f,( - r)))) holds x in ( less_dom ( |.f.|,r))

        proof

          let x be object;

          assume

           A11: x in (( less_dom (f,r)) /\ ( great_dom (f,( - r))));

          then

           A12: x in ( less_dom (f,r)) by XBOOLE_0:def 4;

          

           A13: x in ( great_dom (f,( - r))) by A11, XBOOLE_0:def 4;

          

           A14: x in ( dom f) by A12, MESFUNC1:def 11;

          

           A15: (f . x) < r by A12, MESFUNC1:def 11;

          

           A16: ( - r) < (f . x) by A13, MESFUNC1:def 13;

          reconsider x as Element of X by A11;

          

           A17: x in ( dom |.f.|) by A14, MESFUNC1:def 10;

           |.(f . x).| < r by A15, A16, EXTREAL1: 22;

          then ( |.f.| . x) < r by A17, MESFUNC1:def 10;

          hence thesis by A17, MESFUNC1:def 11;

        end;

        then (( less_dom (f,r)) /\ ( great_dom (f,( - r)))) c= ( less_dom ( |.f.|,r));

        then

         A18: ( less_dom ( |.f.|,r)) = (( less_dom (f,r)) /\ ( great_dom (f,( - r)))) by A10;

        ((A /\ ( great_dom (f,( - r)))) /\ ( less_dom (f,r))) in S by A1, MESFUNC1: 32;

        hence thesis by A18, XBOOLE_1: 16;

      end;

      hence thesis;

    end;

    begin

    definition

      let A,X be set;

      :: original: chi

      redefine

      func chi (A,X) -> PartFunc of X, ExtREAL ;

      coherence

      proof

        now

          let x be object;

          assume

           A1: x in ( rng ( chi (A,X)));

          now

            per cases by A1, TARSKI:def 2;

              suppose x = 0. ;

              hence x in ExtREAL ;

            end;

              suppose x = 1. ;

              hence x in ExtREAL ;

            end;

          end;

          hence x in ExtREAL ;

        end;

        then ( dom ( chi (A,X))) = X & ( rng ( chi (A,X))) c= ExtREAL by FUNCT_3:def 3;

        hence ( chi (A,X)) is PartFunc of X, ExtREAL by RELSET_1: 4;

      end;

    end

    theorem :: MESFUNC2:28

    ( chi (A,X)) is real-valued

    proof

      for x st x in ( dom ( chi (A,X))) holds |.(( chi (A,X)) . x).| < +infty

      proof

        let x;

        assume x in ( dom ( chi (A,X)));

        per cases ;

          suppose x in A;

          then (( chi (A,X)) . x) = 1. by FUNCT_3:def 3;

          then |.(( chi (A,X)) . x).| = jj by EXTREAL1:def 1;

          hence thesis by XXREAL_0: 9;

        end;

          suppose not x in A;

          then (( chi (A,X)) . x) = 0. by FUNCT_3:def 3;

          hence thesis by EXTREAL1:def 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: MESFUNC2:29

    ( chi (A,X)) is B -measurable

    proof

      for r be Real holds (B /\ ( less_eq_dom (( chi (A,X)),r))) in S

      proof

        let r be Real;

        reconsider r as Real;

        now

          per cases ;

            suppose

             A1: r >= 1;

            for x be object st x in X holds x in ( less_eq_dom (( chi (A,X)),r))

            proof

              let x be object;

              assume

               A2: x in X;

              then

               A3: x in ( dom ( chi (A,X))) by FUNCT_3:def 3;

              reconsider x as Element of X by A2;

              (( chi (A,X)) . x) <= 1.

              proof

                now

                  per cases ;

                    suppose x in A;

                    hence thesis by FUNCT_3:def 3;

                  end;

                    suppose not x in A;

                    hence thesis by FUNCT_3:def 3;

                  end;

                end;

                hence thesis;

              end;

              then (( chi (A,X)) . x) <= r by A1, XXREAL_0: 2;

              hence thesis by A3, MESFUNC1:def 12;

            end;

            then X c= ( less_eq_dom (( chi (A,X)),r));

            then ( less_eq_dom (( chi (A,X)),r)) = X;

            then ( less_eq_dom (( chi (A,X)),r)) in S by PROB_1: 5;

            hence thesis by FINSUB_1:def 2;

          end;

            suppose

             A4: 0 <= r & r < 1;

            for x be object st x in ( less_eq_dom (( chi (A,X)),r)) holds x in (X \ A)

            proof

              let x be object;

              assume

               A5: x in ( less_eq_dom (( chi (A,X)),r));

              then

              reconsider x as Element of X;

              (( chi (A,X)) . x) <= r by A5, MESFUNC1:def 12;

              then not x in A by A4, FUNCT_3:def 3;

              hence thesis by XBOOLE_0:def 5;

            end;

            then

             A6: ( less_eq_dom (( chi (A,X)),r)) c= (X \ A);

            for x be object st x in (X \ A) holds x in ( less_eq_dom (( chi (A,X)),r))

            proof

              let x be object;

              assume

               A7: x in (X \ A);

              then

               A8: x in X;

              

               A9: not x in A by A7, XBOOLE_0:def 5;

              reconsider 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 thesis by A4, A10, MESFUNC1:def 12;

            end;

            then (X \ A) c= ( less_eq_dom (( chi (A,X)),r));

            then

             A11: ( less_eq_dom (( chi (A,X)),r)) = (X \ A) by A6;

            X in S by PROB_1: 5;

            then ( less_eq_dom (( chi (A,X)),r)) in S by A11, MEASURE1: 6;

            hence thesis by FINSUB_1:def 2;

          end;

            suppose

             A12: r < 0 ;

            for x holds not x in ( less_eq_dom (( chi (A,X)),r))

            proof

              assume ex x st x in ( less_eq_dom (( chi (A,X)),r));

              then

              consider x such that

               A13: x in ( less_eq_dom (( chi (A,X)),r));

               0. <= (( chi (A,X)) . x)

              proof

                now

                  per cases ;

                    suppose x in A;

                    hence thesis by FUNCT_3:def 3;

                  end;

                    suppose not x in A;

                    hence thesis by FUNCT_3:def 3;

                  end;

                end;

                hence thesis;

              end;

              hence contradiction by A12, A13, MESFUNC1:def 12;

            end;

            then ( less_eq_dom (( chi (A,X)),r)) = {} by SUBSET_1: 4;

            hence thesis by PROB_1: 4;

          end;

        end;

        hence thesis;

      end;

      hence thesis by MESFUNC1: 28;

    end;

    begin

    registration

      let X be set;

      let S be SigmaField of X;

      cluster disjoint_valued for FinSequence of S;

      existence

      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 as FinSequence by FINSEQ_1:def 2;

        ( rng p) c= S by RELAT_1:def 19;

        then

        reconsider p as FinSequence of S by FINSEQ_1:def 4;

        

         A2: for n,m be object st n <> m holds (p . n) misses (p . m)

        proof

          let n,m be object;

          assume n <> m;

          (p . n) = {}

          proof

            per cases ;

              suppose n in ( dom p);

              hence thesis by A1, FUNCOP_1: 7;

            end;

              suppose not n in ( dom p);

              hence thesis by FUNCT_1:def 2;

            end;

          end;

          hence thesis;

        end;

        take p;

        thus thesis by A2, PROB_2:def 2;

      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 :: MESFUNC2:30

    

     Th30: for F be Function st F is Finite_Sep_Sequence of S holds ex G be Sep_Sequence of S st ( union ( rng F)) = ( union ( rng G)) & (for n st n in ( dom F) holds (F . n) = (G . n)) & for m st not m in ( dom F) holds (G . m) = {}

    proof

      let F be Function;

      defpred P[ object, object] 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;

      

       A2: for x1 be object st x1 in NAT holds ex y1 be object st y1 in S & P[x1, y1]

      proof

        let x1 be object;

        assume x1 in NAT ;

        then

        reconsider x1 as Element of NAT ;

        per cases ;

          suppose

           A3: x1 in ( dom F);

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

          thus thesis by A3, A4, A5;

        end;

          suppose

           A6: not x1 in ( dom F);

          take {} ;

          thus thesis by A6, PROB_1: 4;

        end;

      end;

      consider G be sequence of S such that

       A7: for x1 be object st x1 in NAT holds P[x1, (G . x1)] from FUNCT_2:sch 1( A2);

      for n,m be object st n <> m holds (G . n) misses (G . m)

      proof

        let n,m be object;

        assume

         A8: n <> m;

        per cases ;

          suppose

           A9: n in NAT & m in NAT ;

          now

            per cases ;

              suppose n in ( dom F) & m in ( dom F);

              then (G . n) = (F . n) & (G . m) = (F . m) by A7, A9;

              hence thesis by A1, A8, PROB_2:def 2;

            end;

              suppose

               A10: not n in ( dom F) or not m in ( dom F);

              now

                per cases by A10;

                  suppose not n in ( dom F);

                  then (G . n) = {} by A7, A9;

                  hence thesis;

                end;

                  suppose not m in ( dom F);

                  then (G . m) = {} by A7, A9;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          suppose not (n in NAT & m in NAT );

          then not n in ( dom G) or not m in ( dom G);

          then (G . n) = {} or (G . m) = {} by FUNCT_1:def 2;

          hence thesis;

        end;

      end;

      then

      reconsider G as Sep_Sequence of S by PROB_2:def 2;

      take G;

      for x1 be object st x1 in ( union ( rng F)) holds x1 in ( union ( rng G))

      proof

        let x1 be object;

        assume x1 in ( union ( rng F));

        then

        consider Y be set such that

         A11: x1 in Y and

         A12: Y in ( rng F) by TARSKI:def 4;

        consider k be object 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 as Element of NAT by A13;

        

         A15: (F . k) = (G . k) by A7, A13;

        (G . k) in ( rng G) by FUNCT_2: 4;

        hence thesis by A11, A14, A15, TARSKI:def 4;

      end;

      then

       A16: ( union ( rng F)) c= ( union ( rng G));

      for x1 be object st x1 in ( union ( rng G)) holds x1 in ( union ( rng F))

      proof

        let x1 be object;

        assume x1 in ( union ( rng G));

        then

        consider Y be set such that

         A17: x1 in Y and

         A18: Y in ( rng G) by TARSKI:def 4;

        consider k be object such that

         A19: k in ( dom G) and

         A20: Y = (G . k) by A18, FUNCT_1:def 3;

        reconsider 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 thesis by A17, A20, A22, TARSKI:def 4;

      end;

      then ( union ( rng G)) c= ( union ( rng F));

      hence ( union ( rng F)) = ( union ( rng G)) by A16;

      hereby

        let n;

        n in NAT by ORDINAL1:def 12;

        hence n in ( dom F) implies (F . n) = (G . n) by A7;

      end;

      let m;

      m in NAT by ORDINAL1:def 12;

      hence thesis by A7;

    end;

    theorem :: MESFUNC2:31

    for F be Function st F is Finite_Sep_Sequence of S holds ( union ( rng F)) in S

    proof

      let F be Function;

      assume F is Finite_Sep_Sequence of S;

      then ex G be Sep_Sequence of S st ( union ( rng F)) = ( union ( rng G)) & (for n st n in ( dom F) holds (F . n) = (G . n)) & for m st not m in ( dom F) holds (G . m) = {} by Th30;

      hence thesis;

    end;

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      :: MESFUNC2:def4

      pred f is_simple_func_in S means f is real-valued & ex F be Finite_Sep_Sequence of S st (( dom f) = ( union ( rng F)) & for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y));

    end

    theorem :: MESFUNC2:32

    f is real-valued implies ( rng f) is Subset of REAL ;

    theorem :: MESFUNC2:33

    for F be Relation st F is Finite_Sep_Sequence of S holds (F | ( Seg n)) is Finite_Sep_Sequence of S

    proof

      let F be Relation;

      assume

       A1: F is Finite_Sep_Sequence of S;

      then

      reconsider G = (F | ( Seg n)) as FinSequence of S by FINSEQ_1: 18;

      reconsider F as FinSequence of S by A1;

      for k,m be object st k <> m holds (G . k) misses (G . m)

      proof

        let k,m be object;

        assume

         A2: k <> m;

        per cases ;

          suppose k in ( dom G) & m in ( dom G);

          then (G . k) = (F . k) & (G . m) = (F . m) by FUNCT_1: 47;

          hence thesis by A1, A2, PROB_2:def 2;

        end;

          suppose not (k in ( dom G) & m in ( dom G));

          then (G . k) = {} or (G . m) = {} by FUNCT_1:def 2;

          hence thesis;

        end;

      end;

      hence thesis by PROB_2:def 2;

    end;

    theorem :: MESFUNC2:34

    f is_simple_func_in S implies f is A -measurable

    proof

      assume

       A1: f is_simple_func_in S;

      then

      consider F be Finite_Sep_Sequence of S such that

       A2: ( dom f) = ( union ( rng F)) and

       A3: for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y);

      reconsider F as FinSequence of S;

      defpred P[ Nat] means $1 <= ( len F) implies (f | ( union ( rng (F | ( Seg $1))))) is A -measurable;

      

       A4: P[ 0 ]

      proof

        assume

         A5: 0 <= ( len F);

        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 be Real holds (A /\ ( less_dom ((f | ( union ( rng G))),r))) in S

        proof

          let r be Real;

          for x1 be object st x1 in ( less_dom ((f | ( union ( rng G))),r)) holds x1 in ( dom (f | ( union ( rng G)))) by MESFUNC1:def 11;

          then ( less_dom ((f | ( union ( rng G))),r)) c= ( dom (f | ( union ( rng G))));

          then ( less_dom ((f | ( union ( rng G))),r)) = {} by A6, XBOOLE_1: 3;

          hence thesis by PROB_1: 4;

        end;

        hence thesis;

      end;

      

       A7: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        assume

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

        reconsider m as Element of NAT by ORDINAL1:def 12;

        (m + 1) <= ( len F) implies (f | ( union ( rng (F | ( Seg (m + 1)))))) is A -measurable

        proof

          assume

           A9: (m + 1) <= ( len F);

          

           A10: m <= (m + 1) by NAT_1: 11;

          for r be Real holds (A /\ ( less_dom ((f | ( union ( rng (F | ( Seg (m + 1)))))),r))) in S

          proof

            let r be Real;

            now

              per cases ;

                suppose

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

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

                proof

                  reconsider G1 = (F | ( Seg m)) as FinSequence of S by FINSEQ_1: 18;

                  1 <= (m + 1) by NAT_1: 11;

                  then (m + 1) in ( Seg ( len F)) by A9, FINSEQ_1: 1;

                  then (m + 1) in ( dom F) by FINSEQ_1:def 3;

                  then (F | ( Seg (m + 1))) = (G1 ^ <* {} *>) by A11, FINSEQ_5: 10;

                  

                  then ( rng (F | ( Seg (m + 1)))) = (( rng G1) \/ ( rng <* {} *>)) by FINSEQ_1: 31

                  .= (( rng G1) \/ { {} }) by FINSEQ_1: 39;

                  

                  then ( union ( rng (F | ( Seg (m + 1))))) = (( union ( rng G1)) \/ ( union { {} })) by ZFMISC_1: 78

                  .= (( union ( rng G1)) \/ {} ) by ZFMISC_1: 25

                  .= ( union ( rng G1));

                  hence thesis;

                end;

                hence thesis by A8, A9, A10, XXREAL_0: 2;

              end;

                suppose

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

                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 such that

                 A15: x in F1 by A12, SUBSET_1: 4;

                (F | ( Seg (m + 1))) = (G1 ^ <*(F . (m + 1))*>) by A13, FINSEQ_5: 10;

                

                then ( rng (F | ( Seg (m + 1)))) = (( rng G1) \/ ( rng <*(F . (m + 1))*>)) by FINSEQ_1: 31

                .= (( rng G1) \/ {(F . (m + 1))}) by FINSEQ_1: 39;

                

                then

                 A16: ( union ( rng (F | ( Seg (m + 1))))) = (( union ( rng G1)) \/ ( union {(F . (m + 1))})) by ZFMISC_1: 78

                .= (( union ( rng G1)) \/ (F . (m + 1))) by ZFMISC_1: 25;

                

                 A17: x in ( dom f) by A2, A14, A15, TARSKI:def 4;

                f is real-valued by A1;

                then

                 A18: |.(f . x).| < +infty by A17;

                then ( - +infty ) < (f . x) by EXTREAL1: 21;

                then

                 A19: -infty < (f . x) by XXREAL_3:def 3;

                (f . x) < +infty by A18, EXTREAL1: 21;

                then

                reconsider r1 = (f . x) as Element of REAL by A19, XXREAL_0: 14;

                now

                  per cases ;

                    suppose

                     A20: r <= r1;

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

                    proof

                      let x1 be object;

                      assume

                       A21: x1 in ( less_dom ((f | ( union ( rng (F | ( Seg (m + 1)))))),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 as Element of X by A21;

                      

                       A24: ((f | ( union ( rng (F | ( Seg (m + 1)))))) . x1) < r by A21, MESFUNC1:def 11;

                      

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

                      set m1 = (m + 1);

                       not x1 in ( dom (f | F1))

                      proof

                        assume x1 in ( dom (f | F1));

                        then x1 in (( dom f) /\ F1) by RELAT_1: 61;

                        then x1 in (F . m1) by XBOOLE_0:def 4;

                        hence contradiction by A3, A13, A15, A20, A24, A25;

                      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 thesis by A24, A26, MESFUNC1:def 11;

                    end;

                    then

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

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

                    proof

                      let x1 be object;

                      assume

                       A28: x1 in ( less_dom ((f | ( union ( rng (F | ( Seg m))))),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 as Element of X by A28;

                      

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

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

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

                      hence thesis by A33, A34, MESFUNC1:def 11;

                    end;

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

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

                    hence thesis by A8, A9, A10, XXREAL_0: 2;

                  end;

                    suppose

                     A35: r1 < r;

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

                    proof

                      let x1 be object;

                      assume

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

                      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

                        per cases by A38, XBOOLE_0:def 3;

                          suppose

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

                          then

                          reconsider x1 as Element of X;

                          

                           A40: x1 in ( dom (f | ( union ( rng G1)))) by A39, RELAT_1: 61;

                          then

                           A41: ((f | ( union ( rng G1))) . x1) = (f . x1) by FUNCT_1: 47;

                          

                           A42: ((f | ( union ( rng (F | ( Seg (m + 1)))))) . x1) < r by A36, MESFUNC1:def 11;

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

                          then x1 in ( less_dom ((f | ( union ( rng (F | ( Seg m))))),r)) by A40, A42, MESFUNC1:def 11;

                          hence thesis by XBOOLE_0:def 3;

                        end;

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

                          then x1 in (F . (m + 1)) by XBOOLE_0:def 4;

                          hence thesis by XBOOLE_0:def 3;

                        end;

                      end;

                      hence thesis;

                    end;

                    then

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

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

                    proof

                      let x1 be object;

                      assume

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

                      now

                        per cases by A44, XBOOLE_0:def 3;

                          suppose

                           A45: x1 in ( less_dom ((f | ( union ( rng (F | ( Seg m))))),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 as Element of X by A45;

                          

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

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

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

                          hence thesis by A50, A51, MESFUNC1:def 11;

                        end;

                          suppose

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

                          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 as Element of X by A54;

                          

                           A56: (f . x1) = r1 by A3, A13, A15, A52;

                          reconsider y = (f . x1) as R_eal;

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

                          hence thesis by A35, A55, A56, MESFUNC1:def 11;

                        end;

                      end;

                      hence thesis;

                    end;

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

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

                    then

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

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

                    hence thesis by A57, FINSUB_1:def 1;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A58: for n be Nat holds P[n] from NAT_1:sch 2( A4, A7);

      (F | ( Seg ( len F))) = F by FINSEQ_3: 49;

      then (f | ( dom f)) is A -measurable by A2, A58;

      hence thesis by RELAT_1: 68;

    end;