mesfunc7.miz



    begin

    reserve X for non empty set,

S for SigmaField of X,

M for sigma_Measure of S,

f,g for PartFunc of X, ExtREAL ,

E for Element of S;

    theorem :: MESFUNC7:1

    

     Th1: (for x be Element of X st x in ( dom f) holds (f . x) <= (g . x)) implies (g - f) is nonnegative

    proof

      assume

       A1: for x be Element of X st x in ( dom f) holds (f . x) <= (g . x);

      now

        let y be ExtReal;

        assume y in ( rng (g - f));

        then

        consider x be object such that

         A2: x in ( dom (g - f)) and

         A3: y = ((g - f) . x) by FUNCT_1:def 3;

        reconsider x as set by TARSKI: 1;

        ( dom (g - f)) = ((( dom g) /\ ( dom f)) \ (((g " { +infty }) /\ (f " { +infty })) \/ ((g " { -infty }) /\ (f " { -infty })))) by MESFUNC1:def 4;

        then x in (( dom g) /\ ( dom f)) by A2, XBOOLE_0:def 5;

        then x in ( dom f) by XBOOLE_0:def 4;

        then 0. <= ((g . x) - (f . x)) by A1, XXREAL_3: 40;

        hence 0 <= y by A2, A3, MESFUNC1:def 4;

      end;

      then ( rng (g - f)) is nonnegative by SUPINF_2:def 9;

      hence thesis by SUPINF_2:def 12;

    end;

    theorem :: MESFUNC7:2

    

     Th2: for Y be set, f be PartFunc of X, ExtREAL , r be Real holds ((r (#) f) | Y) = (r (#) (f | Y))

    proof

      let Y be set, f be PartFunc of X, ExtREAL , r be Real;

       A1:

      now

        let x be Element of X;

        assume

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

        then

         A3: x in (( dom (r (#) f)) /\ Y) by RELAT_1: 61;

        then

         A4: x in Y by XBOOLE_0:def 4;

        

         A5: x in ( dom (r (#) f)) by A3, XBOOLE_0:def 4;

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

        then x in (( dom f) /\ Y) by A4, XBOOLE_0:def 4;

        then

         A6: x in ( dom (f | Y)) by RELAT_1: 61;

        then

         A7: x in ( dom (r (#) (f | Y))) by MESFUNC1:def 6;

        

        thus (((r (#) f) | Y) . x) = ((r (#) f) . x) by A2, FUNCT_1: 47

        .= (r * (f . x)) by A5, MESFUNC1:def 6

        .= (r * ((f | Y) . x)) by A6, FUNCT_1: 47

        .= ((r (#) (f | Y)) . x) by A7, MESFUNC1:def 6;

      end;

      ( dom ((r (#) f) | Y)) = (( dom (r (#) f)) /\ Y) by RELAT_1: 61

      .= (( dom f) /\ Y) by MESFUNC1:def 6

      .= ( dom (f | Y)) by RELAT_1: 61

      .= ( dom (r (#) (f | Y))) by MESFUNC1:def 6;

      hence thesis by A1, PARTFUN1: 5;

    end;

    reconsider jj = 1 as Real;

    theorem :: MESFUNC7:3

    

     Th3: f is_integrable_on M & g is_integrable_on M & (g - f) is nonnegative implies ex E be Element of S st E = (( dom f) /\ ( dom g)) & ( Integral (M,(f | E))) <= ( Integral (M,(g | E)))

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M and

       A3: (g - f) is nonnegative;

      set h = (( - jj) (#) f);

      

       A4: h is_integrable_on M by A1, MESFUNC5: 110;

      then

      consider E be Element of S such that

       A5: E = (( dom h) /\ ( dom g)) and

       A6: ( Integral (M,(h + g))) = (( Integral (M,(h | E))) + ( Integral (M,(g | E)))) by A2, MESFUNC5: 109;

      

       A7: ex E3 be Element of S st E3 = ( dom h) & h is E3 -measurable by A4;

      

       A8: (g | E) is_integrable_on M by A2, MESFUNC5: 97;

      then

       A9: ( Integral (M,(g | E))) < +infty by MESFUNC5: 96;

       -infty < ( Integral (M,(g | E))) by A8, MESFUNC5: 96;

      then

      reconsider c2 = ( Integral (M,(g | E))) as Element of REAL by A9, XXREAL_0: 14;

      take E;

      

       A10: (h | E) = (( - jj) (#) (f | E)) by Th2;

      (g + ( - f)) is nonnegative by A3, MESFUNC2: 8;

      then

       A11: (h + g) is nonnegative by MESFUNC2: 9;

      

       A12: (f | E) is_integrable_on M by A1, MESFUNC5: 97;

      then

       A13: ( Integral (M,(f | E))) < +infty by MESFUNC5: 96;

       -infty < ( Integral (M,(f | E))) by A12, MESFUNC5: 96;

      then

      reconsider c1 = ( Integral (M,(f | E))) as Element of REAL by A13, XXREAL_0: 14;

      

       A14: (( - jj) qua ExtReal * ( Integral (M,(f | E)))) = (( - jj) * c1) by EXTREAL1: 1

      .= ( - c1);

      ex E2 be Element of S st E2 = ( dom g) & g is E2 -measurable by A2;

      then ex A be Element of S st A = ( dom (h + g)) & (h + g) is A -measurable by A7, MESFUNC5: 47;

      then 0 <= (( Integral (M,(h | E))) + ( Integral (M,(g | E)))) by A6, A11, MESFUNC5: 90;

      then 0 <= ((( - jj) qua ExtReal * ( Integral (M,(f | E)))) + ( Integral (M,(g | E)))) by A12, A10, MESFUNC5: 110;

      then 0 <= (( - c1) + c2) by A14, XXREAL_3:def 2;

      then ( 0 + c1) <= ((( - c1) + c2) + c1) by XREAL_1: 6;

      hence thesis by A5, MESFUNC1:def 6;

    end;

    begin

    registration

      let X;

      cluster nonnegative for PartFunc of X, ExtREAL ;

      existence

      proof

        set f = the PartFunc of X, ExtREAL ;

        take |.f.|;

        now

          let x be object;

          assume x in ( dom |.f.|);

          then ( |.f.| . x) = |.(f . x).| by MESFUNC1:def 10;

          hence 0. <= ( |.f.| . x) by EXTREAL1: 14;

        end;

        hence thesis by SUPINF_2: 52;

      end;

    end

    registration

      let X, f;

      cluster |.f.| -> nonnegative;

      correctness

      proof

        now

          let x be object;

          assume x in ( dom |.f.|);

          then ( |.f.| . x) = |.(f . x).| by MESFUNC1:def 10;

          hence 0. <= ( |.f.| . x) by EXTREAL1: 14;

        end;

        hence thesis by SUPINF_2: 52;

      end;

    end

    theorem :: MESFUNC7:4

    f is_integrable_on M implies ex F be sequence of S st (for n be Element of NAT holds (F . n) = (( dom f) /\ ( great_eq_dom ( |.f.|,(1 / (n + 1)))))) & (( dom f) \ ( eq_dom (f, 0. ))) = ( union ( rng F)) & for n be Element of NAT holds (F . n) in S & (M . (F . n)) < +infty

    proof

      assume

       A1: f is_integrable_on M;

      then

      consider E be Element of S such that

       A2: E = ( dom f) and

       A3: f is E -measurable;

      defpred P[ Element of NAT , set] means $2 = (E /\ ( great_eq_dom ( |.f.|,(1 / ($1 + 1)))));

      

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

      now

        let x be object;

        assume

         A5: x in (E \ ( eq_dom (f, 0. )));

        then

        reconsider z = x as Element of X;

        reconsider y = (f . z) as R_eal;

        

         A6: x in E by A5, XBOOLE_0:def 5;

        then

         A7: x in ( dom |.f.|) by A2, MESFUNC1:def 10;

         not x in ( eq_dom (f, 0. )) by A5, XBOOLE_0:def 5;

        then not y = 0. by A2, A6, MESFUNC1:def 15;

        then 0. < |.(f . z).| by EXTREAL1: 15;

        then 0. < ( |.f.| . z) by A7, MESFUNC1:def 10;

        then x in ( great_dom ( |.f.|, 0. )) by A7, MESFUNC1:def 13;

        hence x in (E /\ ( great_dom ( |.f.|, 0. ))) by A6, XBOOLE_0:def 4;

      end;

      then

       A8: (E \ ( eq_dom (f, 0. ))) c= (E /\ ( great_dom ( |.f.|, 0. )));

      now

        let x be object;

        assume

         A9: x in (E /\ ( great_dom ( |.f.|, 0. )));

        then

        reconsider z = x as Element of X;

        x in ( great_dom ( |.f.|, 0. )) by A9, XBOOLE_0:def 4;

        then

         A10: 0. < ( |.f.| . z) by MESFUNC1:def 13;

        

         A11: x in E by A9, XBOOLE_0:def 4;

        then x in ( dom |.f.|) by A2, MESFUNC1:def 10;

        then

         A12: 0. < |.(f . z).| by A10, MESFUNC1:def 10;

         not x in ( eq_dom (f, 0. ))

        proof

          assume x in ( eq_dom (f, 0. ));

          then (f . z) = 0. by MESFUNC1:def 15;

          hence contradiction by A12, EXTREAL1: 16;

        end;

        hence x in (E \ ( eq_dom (f, 0. ))) by A11, XBOOLE_0:def 5;

      end;

      then

       A13: (E /\ ( great_dom ( |.f.|, 0. ))) c= (E \ ( eq_dom (f, 0. )));

      

       A14: |.f.| is E -measurable by A2, A3, MESFUNC2: 27;

      

       A15: for n be Element of NAT holds ex Z be Element of S st P[n, Z]

      proof

        let n be Element of NAT ;

        take (E /\ ( great_eq_dom ( |.f.|,(1 / (n + 1)))));

        thus thesis by A14, A4, MESFUNC1: 27;

      end;

      consider F be sequence of S such that

       A16: for n be Element of NAT holds P[n, (F . n)] from FUNCT_2:sch 3( A15);

      

       A17: for n be Element of NAT holds (F . n) in S & (M . (F . n)) < +infty

      proof

        let n be Element of NAT ;

        set d = (1 / (n + 1));

        set En = (F . n);

        set g = ( |.f.| | En);

        

         A18: g is nonnegative by MESFUNC5: 15;

        set z = (1 / (n + 1));

        

         A19: ( |.f.| | E) = |.f.| by A4, RELAT_1: 69;

        

         A20: (F . n) = (E /\ ( great_eq_dom ( |.f.|,(1 / (n + 1))))) by A16;

        then

         A21: ( dom g) = En by A4, RELAT_1: 62, XBOOLE_1: 17;

        (( dom |.f.|) /\ En) = (E /\ En) by A2, MESFUNC1:def 10;

        then

         A22: (( dom |.f.|) /\ En) = En by A20, XBOOLE_1: 17, XBOOLE_1: 28;

         |.f.| is En -measurable by A14, A20, MESFUNC1: 30, XBOOLE_1: 17;

        then

         A23: g is En -measurable by A22, MESFUNC5: 42;

        then

         A24: ( integral+ (M,g)) = ( Integral (M,g)) by A21, MESFUNC5: 15, MESFUNC5: 88;

         |.f.| is_integrable_on M by A1, MESFUNC5: 100;

        then

         A25: ( Integral (M, |.f.|)) < +infty by MESFUNC5: 96;

        

         A26: ((z * (M . En)) / z) = (M . En) by XXREAL_3: 88;

        (F . n) c= E by A20, XBOOLE_1: 17;

        then

         A27: ( Integral (M,g)) <= ( Integral (M, |.f.|)) by A2, A3, A4, A19, MESFUNC2: 27, MESFUNC5: 93;

        consider nf be PartFunc of X, ExtREAL such that

         A28: nf is_simple_func_in S and

         A29: ( dom nf) = En and

         A30: for x be object st x in En holds (nf . x) = d by MESFUNC5: 41;

        for x be object st x in ( dom nf) holds (nf . x) >= 0 by A29, A30;

        then

         A31: nf is nonnegative by SUPINF_2: 52;

        then

         A32: ( Integral (M,nf)) = ( integral' (M,nf)) by A28, MESFUNC5: 89;

        

         A33: (F . n) c= ( great_eq_dom ( |.f.|,(1 / (n + 1)))) by A20, XBOOLE_1: 17;

        

         A34: for x be Element of X st x in ( dom nf) holds (nf . x) <= (g . x)

        proof

          let x be Element of X;

          assume

           A35: x in ( dom nf);

          then

           A36: (1 / (n + 1)) <= ( |.f.| . x) by A33, A29, MESFUNC1:def 14;

          (g . x) = ( |.f.| . x) by A21, A29, A35, FUNCT_1: 47;

          hence thesis by A29, A30, A35, A36;

        end;

        nf is En -measurable by A28, MESFUNC2: 34;

        then ( integral+ (M,nf)) <= ( integral+ (M,g)) by A21, A23, A18, A29, A31, A34, MESFUNC5: 85;

        then

         A37: ( integral+ (M,nf)) <= ( Integral (M, |.f.|)) by A24, A27, XXREAL_0: 2;

        

         A38: ( +infty / z) = +infty by XXREAL_3: 83;

        ( integral+ (M,nf)) = ( Integral (M,nf)) by A28, A31, MESFUNC5: 89;

        then ( integral+ (M,nf)) = ((1 / (n + 1)) * (M . En)) by A29, A30, A32, MESFUNC5: 104;

        then ((1 / (n + 1)) * (M . En)) < +infty by A25, A37, XXREAL_0: 2;

        hence thesis by A26, A38, XXREAL_3: 80;

      end;

      take F;

      for n be Element of NAT holds (F . n) = (E /\ ( great_eq_dom ( |.f.|,( 0 + (1 / (n + 1)))))) by A16;

      then (E /\ ( great_dom ( |.f.|, 0 ))) = ( union ( rng F)) by MESFUNC1: 22;

      hence thesis by A2, A16, A13, A8, A17, XBOOLE_0:def 10;

    end;

    begin

    notation

      let F be Relation;

      synonym F is extreal-yielding for F is ext-real-valued;

    end

    registration

      cluster extreal-yielding for FinSequence;

      existence

      proof

        set f = the FinSequence of ExtREAL ;

        f is extreal-yielding;

        hence thesis;

      end;

    end

    definition

      :: MESFUNC7:def1

      func multextreal -> BinOp of ExtREAL means

      : Def1: for x,y be Element of ExtREAL holds (it . (x,y)) = (x * y);

      existence from BINOP_1:sch 4;

      uniqueness from BINOP_2:sch 2;

    end

    registration

      cluster multextreal -> commutative associative;

      coherence

      proof

        

         A1: for a,b,c be Element of ExtREAL holds ( multextreal . (a,( multextreal . (b,c)))) = ( multextreal . (( multextreal . (a,b)),c))

        proof

          let a,b,c be Element of ExtREAL ;

          ( multextreal . (a,( multextreal . (b,c)))) = ( multextreal . (a,(b * c))) by Def1;

          then ( multextreal . (a,( multextreal . (b,c)))) = (a * (b * c)) by Def1;

          then ( multextreal . (a,( multextreal . (b,c)))) = ((a * b) * c) by XXREAL_3: 66;

          then ( multextreal . (a,( multextreal . (b,c)))) = ( multextreal . ((a * b),c)) by Def1;

          hence thesis by Def1;

        end;

        for a,b be Element of ExtREAL holds ( multextreal . (a,b)) = ( multextreal . (b,a))

        proof

          let a,b be Element of ExtREAL ;

          ( multextreal . (a,b)) = (a * b) by Def1;

          hence thesis by Def1;

        end;

        hence thesis by A1, BINOP_1:def 2, BINOP_1:def 3;

      end;

    end

    

     Lm1: 1. is_a_unity_wrt multextreal

    proof

      for r be Element of ExtREAL holds ( multextreal . (r, 1. )) = r

      proof

        let r be Element of ExtREAL ;

        ( multextreal . (r, 1. )) = (r * 1. ) by Def1;

        hence thesis by XXREAL_3: 81;

      end;

      then

       A1: 1. is_a_right_unity_wrt multextreal by BINOP_1:def 6;

      for r be Element of ExtREAL holds ( multextreal . ( 1. ,r)) = r

      proof

        let r be Element of ExtREAL ;

        ( multextreal . ( 1. ,r)) = ( 1. * r) by Def1;

        hence thesis by XXREAL_3: 81;

      end;

      then 1. is_a_left_unity_wrt multextreal by BINOP_1:def 5;

      hence thesis by A1, BINOP_1:def 7;

    end;

    theorem :: MESFUNC7:5

    

     Th5: ( the_unity_wrt multextreal ) = 1 by Lm1, BINOP_1:def 8;

    registration

      cluster multextreal -> having_a_unity;

      coherence by Lm1, Th5, SETWISEO: 14;

    end

    definition

      let F be extreal-yielding FinSequence;

      :: MESFUNC7:def2

      func Product F -> Element of ExtREAL means

      : Def2: ex f be FinSequence of ExtREAL st f = F & it = ( multextreal $$ f);

      existence

      proof

        ( rng F) c= ExtREAL by VALUED_0:def 2;

        then

        reconsider f = F as FinSequence of ExtREAL by FINSEQ_1:def 4;

        take ( multextreal $$ f);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let x be Element of ExtREAL , n be Nat;

      cluster (n |-> x) -> extreal-yielding;

      coherence ;

    end

    definition

      let x be Element of ExtREAL ;

      let k be Nat;

      :: MESFUNC7:def3

      func x |^ k -> number equals ( Product (k |-> x));

      coherence ;

    end

    definition

      let x be Element of ExtREAL , k be Nat;

      :: original: |^

      redefine

      func x |^ k -> R_eal ;

      coherence ;

    end

    registration

      cluster ( <*> ExtREAL ) -> extreal-yielding;

      coherence ;

    end

    registration

      let r be Element of ExtREAL ;

      cluster <*r*> -> extreal-yielding;

      coherence ;

    end

    theorem :: MESFUNC7:6

    

     Th6: ( Product ( <*> ExtREAL )) = 1

    proof

      ( Product ( <*> ExtREAL )) = ( multextreal $$ ( <*> ExtREAL )) by Def2;

      hence thesis by Th5, FINSOP_1: 10;

    end;

    theorem :: MESFUNC7:7

    

     Th7: for r be Element of ExtREAL holds ( Product <*r*>) = r

    proof

      let r be Element of ExtREAL ;

      reconsider r9 = r as Element of ExtREAL ;

      reconsider F = <*r9*> as FinSequence of ExtREAL ;

      ( multextreal $$ F) = r by FINSOP_1: 11;

      hence thesis by Def2;

    end;

    registration

      let f,g be extreal-yielding FinSequence;

      cluster (f ^ g) -> extreal-yielding;

      coherence

      proof

        

         A1: ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by FINSEQ_1: 31;

        

         A2: ( rng g) c= ExtREAL by VALUED_0:def 2;

        ( rng f) c= ExtREAL by VALUED_0:def 2;

        then ( rng (f ^ g)) c= ExtREAL by A2, A1, XBOOLE_1: 8;

        hence thesis by VALUED_0:def 2;

      end;

    end

    theorem :: MESFUNC7:8

    

     Th8: for F be extreal-yielding FinSequence, r be Element of ExtREAL holds ( Product (F ^ <*r*>)) = (( Product F) * r)

    proof

      let F be extreal-yielding FinSequence, r be Element of ExtREAL ;

      

       A1: ( rng (F ^ <*r*>)) c= ExtREAL by VALUED_0:def 2;

      ( rng F) c= ExtREAL by VALUED_0:def 2;

      then

      reconsider Fr = (F ^ <*r*>), Ff = F as FinSequence of ExtREAL by A1, FINSEQ_1:def 4;

      reconsider Ff1 = Ff as extreal-yielding FinSequence;

      ( Product (F ^ <*r*>)) = ( multextreal $$ Fr) by Def2;

      then ( Product (F ^ <*r*>)) = ( multextreal . (( multextreal $$ Ff),r)) by FINSOP_1: 4;

      then ( Product (F ^ <*r*>)) = ( multextreal . (( Product Ff1),r)) by Def2;

      hence thesis by Def1;

    end;

    theorem :: MESFUNC7:9

    

     Th9: for x be Element of ExtREAL holds (x |^ 1) = x

    proof

      let x be Element of ExtREAL ;

      ( Product (1 |-> x)) = ( Product <*x*>) by FINSEQ_2: 59;

      hence thesis by Th7;

    end;

    theorem :: MESFUNC7:10

    

     Th10: for x be Element of ExtREAL , k be Nat holds (x |^ (k + 1)) = ((x |^ k) * x)

    proof

      let x be Element of ExtREAL ;

      defpred P[ Nat] means (x |^ ($1 + 1)) = ((x |^ $1) * x);

      

       A1: for k be Nat st P[k] holds P[(k + 1 qua Complex)]

      proof

        let k be Nat;

        assume (x |^ (k + 1)) = ((x |^ k) * x);

        reconsider k1 = (k + 1) as Element of NAT ;

        ( Product ((k1 + 1) |-> x)) = ( Product ((k1 |-> x) ^ <*x*>)) by FINSEQ_2: 60;

        hence thesis by Th8;

      end;

      (x |^ ( 0 + 1)) = ( Product <*x*>) by FINSEQ_2: 59;

      then (x |^ ( 0 + 1)) = x by Th7;

      then (x |^ ( 0 + 1)) = ( 1. * x) by XXREAL_3: 81;

      then

       A2: P[ 0 ] by Th6, FINSEQ_2: 58;

      for k be Nat holds P[k] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    definition

      let k be Nat, X, f;

      :: MESFUNC7:def4

      func f |^ k -> PartFunc of X, ExtREAL means

      : Def4: ( dom it ) = ( dom f) & for x be Element of X st x in ( dom it ) holds (it . x) = ((f . x) |^ k);

      existence

      proof

        deffunc U( set) = ((f . $1) |^ k);

        defpred X[ set] means $1 in ( dom f);

        consider f3 be PartFunc of X, ExtREAL such that

         A1: for d be Element of X holds d in ( dom f3) iff X[d] and

         A2: for d be Element of X st d in ( dom f3) holds (f3 /. d) = U(d) from PARTFUN2:sch 2;

        take f3;

        for x be object st x in ( dom f) holds x in ( dom f3) by A1;

        then

         A3: ( dom f) c= ( dom f3);

        for x be object st x in ( dom f3) holds x in ( dom f) by A1;

        then ( dom f3) c= ( dom f);

        hence ( dom f3) = ( dom f) by A3, XBOOLE_0:def 10;

        let d be Element of X;

        assume

         A4: d in ( dom f3);

        then (f3 /. d) = ((f . d) |^ k) by A2;

        hence thesis by A4, PARTFUN1:def 6;

      end;

      uniqueness

      proof

        let f1,f2 be PartFunc of X, ExtREAL ;

        assume that

         A5: ( dom f1) = ( dom f) and

         A6: for d be Element of X st d in ( dom f1) holds (f1 . d) = ((f . d) |^ k) and

         A7: ( dom f2) = ( dom f) and

         A8: for d be Element of X st d in ( dom f2) holds (f2 . d) = ((f . d) |^ k);

        for d be Element of X st d in ( dom f) holds (f1 . d) = (f2 . d)

        proof

          let d be Element of X;

          assume

           A9: d in ( dom f);

          then (f1 . d) = ((f . d) |^ k) by A5, A6;

          hence thesis by A7, A8, A9;

        end;

        hence f1 = f2 by A5, A7, PARTFUN1: 5;

      end;

    end

    theorem :: MESFUNC7:11

    

     Th11: for x be Element of ExtREAL , y be Real, k be Nat st x = y holds (x |^ k) = (y |^ k)

    proof

      let x be Element of ExtREAL , y be Real, k be Nat;

      defpred P[ Nat] means (x |^ $1) = (y |^ $1);

      assume

       A1: x = y;

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

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

        let k be Nat;

        assume P[k];

        then ((x |^ k) * x) = ((y |^ k) * y) by A1, EXTREAL1: 1;

        then ((x |^ k) * x) = (y |^ (k + 1)) by NEWTON: 6;

        hence thesis by Th10;

      end;

      (x |^ 0 ) = 1. by Th6, FINSEQ_2: 58;

      then

       A3: P[ 0 ] by NEWTON: 4;

      for k be Nat holds P[k] from NAT_1:sch 2( A3, A2);

      hence thesis;

    end;

    theorem :: MESFUNC7:12

    

     Th12: for x be Element of ExtREAL , k be Nat st 0 <= x holds 0 <= (x |^ k)

    proof

      let x be Element of ExtREAL , k be Nat;

      defpred P[ Nat] means 0 <= (x |^ $1);

      assume

       A1: 0 <= x;

      

       A2: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A3: P[k];

        (x |^ (k + 1)) = ((x |^ k) * x) by Th10;

        hence thesis by A1, A3;

      end;

      

       A4: P[ 0 ] by Th6, FINSEQ_2: 58;

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: MESFUNC7:13

    

     Th13: for k be Nat st 1 <= k holds ( +infty |^ k) = +infty

    proof

      defpred P[ Nat] means ( +infty |^ $1) = +infty ;

      

       A1: for k be non zero Nat st P[k] holds P[(k + 1)]

      proof

        let k be non zero Nat;

        assume

         A2: P[k];

        ( +infty |^ (k + 1)) = (( +infty |^ k) * +infty ) by Th10;

        hence thesis by A2, XXREAL_3:def 5;

      end;

      

       A3: P[1] by Th9;

      for k be non zero Nat holds P[k] from NAT_1:sch 10( A3, A1);

      hence thesis;

    end;

    theorem :: MESFUNC7:14

    

     Th14: for k be Nat, X, S, f, E st E c= ( dom f) & f is E -measurable holds ( |.f.| |^ k) is E -measurable

    proof

      let k be Nat;

      let X, S, f, E;

      reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

      assume that

       A1: E c= ( dom f) and

       A2: f is E -measurable;

      

       A3: ( dom ( |.f.| |^ k)) = ( dom |.f.|) by Def4;

      then

       A4: ( dom ( |.f.| |^ k)) = ( dom f) by MESFUNC1:def 10;

      per cases ;

        suppose

         A5: k = 0 ;

        

         A6: for r be Real st 1 < r holds (E /\ ( less_dom (( |.f.| |^ k),r))) in S

        proof

          let r be Real;

          assume

           A7: 1 < r;

          E c= ( less_dom (( |.f.| |^ k),r))

          proof

            let x be object;

            reconsider xx = x as set by TARSKI: 1;

            assume

             A8: x in E;

            then (( |.f.| |^ k) . xx) = (( |.f.| . xx) |^ k) by A1, A4, Def4;

            then (( |.f.| |^ k) . xx) < r by A5, A7, Th6, FINSEQ_2: 58;

            hence thesis by A1, A4, A8, MESFUNC1:def 11;

          end;

          then (E /\ ( less_dom (( |.f.| |^ k),r))) = E by XBOOLE_1: 28;

          hence thesis;

        end;

        

         A9: E c= ( dom ( |.f.| |^ k)) by A1, A3, MESFUNC1:def 10;

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

        proof

          let r be Real;

          now

            assume

             A10: r <= 1;

            E c= ( great_eq_dom (( |.f.| |^ k),r))

            proof

              let x be object;

              reconsider xx = x as set by TARSKI: 1;

              assume

               A11: x in E;

              then (( |.f.| |^ k) . xx) = (( |.f.| . xx) |^ k) by A1, A4, Def4;

              then r <= (( |.f.| |^ k) . xx) by A5, A10, Th6, FINSEQ_2: 58;

              hence thesis by A1, A4, A11, MESFUNC1:def 14;

            end;

            then (E /\ ( great_eq_dom (( |.f.| |^ k),r))) = E by XBOOLE_1: 28;

            then (E /\ ( less_dom (( |.f.| |^ k),r))) = (E \ E) by A9, MESFUNC1: 17;

            hence thesis;

          end;

          hence thesis by A6;

        end;

        hence thesis;

      end;

        suppose

         A12: k <> 0 ;

        then

         A13: ((jj / k) * k) = 1 by XCMPLX_1: 87;

        

         A14: for r be Real st 0 < r holds ( great_eq_dom (( |.f.| |^ k),r)) = ( great_eq_dom ( |.f.|,(r to_power (1 / k))))

        proof

          let r be Real;

          assume

           A15: 0 < r;

          

           A16: ( great_eq_dom (( |.f.| |^ k),r)) c= ( great_eq_dom ( |.f.|,(r to_power (1 / k))))

          proof

            let x be object;

            reconsider xx = x as set by TARSKI: 1;

            assume

             A17: x in ( great_eq_dom (( |.f.| |^ k),r));

            then

             A18: x in ( dom ( |.f.| |^ k)) by MESFUNC1:def 14;

            then

             A19: ( |.f.| . xx) = |.(f . xx).| by A3, MESFUNC1:def 10;

            then

             A20: 0 <= ( |.f.| . xx) by EXTREAL1: 14;

            per cases ;

              suppose ( |.f.| . xx) = +infty ;

              then (r to_power (1 / k)) <= ( |.f.| . xx) by XXREAL_0: 3;

              hence thesis by A3, A18, MESFUNC1:def 14;

            end;

              suppose ( |.f.| . xx) <> +infty ;

              then

              reconsider fx = ( |.f.| . xx) as Element of REAL by A20, XXREAL_0: 14;

              

               A21: r <= (( |.f.| |^ k) . xx) by A17, MESFUNC1:def 14;

              (( |.f.| |^ k) . xx) = (( |.f.| . xx) |^ k) by A18, Def4;

              then

               A22: r <= (fx to_power k1) by A21, Th11;

              ((fx to_power k) to_power (jj / k)) = (fx to_power ((k * jj) / k)) by A12, A19, EXTREAL1: 14, HOLDER_1: 2;

              then

               A23: ((fx to_power k) to_power (1 / k)) = fx by A13, POWER: 25;

              (r to_power (jj / k)) <= ((fx to_power k) to_power (jj / k)) by A15, A22, HOLDER_1: 3;

              hence thesis by A3, A18, A23, MESFUNC1:def 14;

            end;

          end;

          ( great_eq_dom ( |.f.|,(r to_power (1 / k)))) c= ( great_eq_dom (( |.f.| |^ k),r))

          proof

            let x be object;

            reconsider xx = x as set by TARSKI: 1;

            assume

             A24: x in ( great_eq_dom ( |.f.|,(r to_power (1 / k))));

            then

             A25: x in ( dom |.f.|) by MESFUNC1:def 14;

            then

             A26: (( |.f.| |^ k) . xx) = (( |.f.| . xx) |^ k) by A3, Def4;

            ( |.f.| . xx) = |.(f . xx).| by A25, MESFUNC1:def 10;

            then

             A27: 0 <= ( |.f.| . xx) by EXTREAL1: 14;

             A28:

            now

              assume ( |.f.| . xx) <> +infty ;

              then

              reconsider fx = ( |.f.| . xx) as Element of REAL by A27, XXREAL_0: 14;

              reconsider R = (r to_power (1 / k)) as Real;

              

               A29: 0 < (r to_power (1 / k)) by A15, POWER: 34;

              

               A30: (R to_power k1) = (r to_power ((jj / k) * k)) by A15, POWER: 33;

              

               A31: (( |.f.| |^ k) . xx) = (fx |^ k) by A26, Th11;

              (r to_power (1 / k)) <= ( |.f.| . xx) by A24, MESFUNC1:def 14;

              then (r to_power 1) <= (fx to_power k) by A13, A29, A30, HOLDER_1: 3;

              hence r <= (( |.f.| |^ k) . xx) by A31;

            end;

            now

              assume ( |.f.| . xx) = +infty ;

              then (( |.f.| . xx) |^ k) = +infty by A12, Th13, NAT_1: 14;

              hence r <= (( |.f.| |^ k) . xx) by A26, XXREAL_0: 3;

            end;

            hence thesis by A3, A25, A28, MESFUNC1:def 14;

          end;

          hence thesis by A16, XBOOLE_0:def 10;

        end;

        

         A32: |.f.| is E -measurable by A1, A2, MESFUNC2: 27;

        for r be Real holds (E /\ ( great_eq_dom (( |.f.| |^ k),r))) in S

        proof

          let r be Real;

          per cases ;

            suppose

             A33: r <= 0 ;

            E c= ( great_eq_dom (( |.f.| |^ k),r))

            proof

              let x be object;

              reconsider xx = x as set by TARSKI: 1;

              assume

               A34: x in E;

              then

               A35: ( |.f.| . xx) = |.(f . xx).| by A1, A3, A4, MESFUNC1:def 10;

              (( |.f.| |^ k) . xx) = (( |.f.| . xx) |^ k) by A1, A4, A34, Def4;

              then r <= (( |.f.| |^ k) . xx) by A33, A35, Th12, EXTREAL1: 14;

              hence thesis by A1, A4, A34, MESFUNC1:def 14;

            end;

            then (E /\ ( great_eq_dom (( |.f.| |^ k),r))) = E by XBOOLE_1: 28;

            hence thesis;

          end;

            suppose 0 < r;

            then (E /\ ( great_eq_dom (( |.f.| |^ k),r))) = (E /\ ( great_eq_dom ( |.f.|,(r to_power (1 / k))))) by A14;

            hence thesis by A1, A3, A4, A32, MESFUNC1: 27;

          end;

        end;

        hence thesis by A1, A4, MESFUNC1: 27;

      end;

    end;

    theorem :: MESFUNC7:15

    

     Th15: (( dom f) /\ ( dom g)) = E & f is real-valued & g is real-valued & f is E -measurable & g is E -measurable implies (f (#) g) is E -measurable

    proof

      assume that

       A1: (( dom f) /\ ( dom g)) = E and

       A2: f is real-valued and

       A3: g is real-valued and

       A4: f is E -measurable and

       A5: g is E -measurable;

      

       A6: ( dom (f (#) g)) = (( dom f) /\ ( dom g)) by MESFUNC1:def 5;

      

       A7: ( dom ((1 / 4) (#) ( |.(f + g).| |^ 2))) = ( dom ( |.(f + g).| |^ 2)) by MESFUNC1:def 6;

      

       A8: ( dom ( |.(f - g).| |^ 2)) = ( dom |.(f - g).|) by Def4;

      then

       A9: ( dom ( |.(f - g).| |^ 2)) = ( dom (f - g)) by MESFUNC1:def 10;

      then

       A10: ( dom ( |.(f - g).| |^ 2)) = (( dom f) /\ ( dom g)) by A2, MESFUNC2: 2;

      then

       A11: ( dom ( |.(f - g).| |^ 2)) c= ( dom g) by XBOOLE_1: 17;

      

       A12: ( dom ((1 / 4) (#) ( |.(f - g).| |^ 2))) = ( dom ( |.(f - g).| |^ 2)) by MESFUNC1:def 6;

      

       A13: ( dom ( |.(f + g).| |^ 2)) = ( dom |.(f + g).|) by Def4;

      then

       A14: ( dom ( |.(f + g).| |^ 2)) = ( dom (f + g)) by MESFUNC1:def 10;

      then

       A15: ( dom ( |.(f + g).| |^ 2)) = (( dom f) /\ ( dom g)) by A2, MESFUNC2: 2;

      then

       A16: ( dom ( |.(f + g).| |^ 2)) c= ( dom g) by XBOOLE_1: 17;

      

       A17: ( dom ( |.(f + g).| |^ 2)) c= ( dom f) by A15, XBOOLE_1: 17;

      for x be Element of X st x in ( dom ( |.(f + g).| |^ 2)) holds |.(( |.(f + g).| |^ 2) . x).| < +infty

      proof

        let x be Element of X;

        assume

         A18: x in ( dom ( |.(f + g).| |^ 2));

        then

         A19: |.(g . x).| < +infty by A3, A16, MESFUNC2:def 1;

         |.(f . x).| < +infty by A2, A17, A18, MESFUNC2:def 1;

        then

        reconsider c1 = (f . x), c2 = (g . x) as Element of REAL by A19, EXTREAL1: 41;

        ((f . x) + (g . x)) = (c1 + c2) by SUPINF_2: 1;

        then |.((f . x) + (g . x)).| = |.(c1 + c2) qua Complex.| by EXTREAL1: 12;

        then

         A20: ( |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|) = ( |.(c1 + c2) qua Complex.| * |.(c1 + c2) qua Complex.|) by EXTREAL1: 1;

        (( |.(f + g).| |^ 2) . x) = (( |.(f + g).| . x) |^ (1 + 1)) by A18, Def4;

        then

         A21: (( |.(f + g).| |^ 2) . x) = ((( |.(f + g).| . x) |^ 1) * ( |.(f + g).| . x)) by Th10;

        

         A22: |.((f + g) . x).| = |.((f . x) + (g . x)).| by A14, A18, MESFUNC1:def 3;

        ( |.(f + g).| . x) = |.((f + g) . x).| by A13, A18, MESFUNC1:def 10;

        

        then |.(( |.(f + g).| |^ 2) . x).| = |.( |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|).| by A21, A22, Th9

        .= |. |.(((f . x) + (g . x)) * ((f . x) + (g . x))).|.| by EXTREAL1: 19

        .= |.(((f . x) + (g . x)) * ((f . x) + (g . x))).|

        .= ( |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|) by EXTREAL1: 19;

        hence thesis by A20, XXREAL_0: 9, XREAL_0:def 1;

      end;

      then ( |.(f + g).| |^ 2) is real-valued by MESFUNC2:def 1;

      then

       A23: ((1 / 4) (#) ( |.(f + g).| |^ 2)) is real-valued by MESFUNC2: 10;

      then

       A24: ( dom (((1 / 4) (#) ( |.(f + g).| |^ 2)) - ((1 / 4) (#) ( |.(f - g).| |^ 2)))) = (( dom ((1 / 4) (#) ( |.(f + g).| |^ 2))) /\ ( dom ((1 / 4) (#) ( |.(f - g).| |^ 2)))) by MESFUNC2: 2;

      for x be Element of X st x in ( dom (f (#) g)) holds ((f (#) g) . x) = ((((1 / 4) (#) ( |.(f + g).| |^ 2)) - ((1 / 4) (#) ( |.(f - g).| |^ 2))) . x)

      proof

        let x be Element of X;

        assume

         A25: x in ( dom (f (#) g));

        then

         A26: |.(g . x).| < +infty by A3, A15, A16, A6, MESFUNC2:def 1;

         |.(f . x).| < +infty by A2, A15, A17, A6, A25, MESFUNC2:def 1;

        then

        reconsider c1 = (f . x), c2 = (g . x) as Element of REAL by A26, EXTREAL1: 41;

        ((f . x) + (g . x)) = (c1 + c2) by SUPINF_2: 1;

        then |.((f . x) + (g . x)).| = |.(c1 + c2) qua Complex.| by EXTREAL1: 12;

        then

         A27: ( |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|) = ( |.(c1 + c2) qua Complex.| * |.(c1 + c2) qua Complex.|) by EXTREAL1: 1;

        (((1 / 4) (#) ( |.(f + g).| |^ 2)) . x) = ((1 / 4) * (( |.(f + g).| |^ 2) . x)) by A15, A6, A7, A25, MESFUNC1:def 6;

        then (((1 / 4) (#) ( |.(f + g).| |^ 2)) . x) = ((1 / 4) * (( |.(f + g).| . x) |^ (1 + 1))) by A15, A6, A25, Def4;

        then

         A28: (((1 / 4) (#) ( |.(f + g).| |^ 2)) . x) = ((1 / 4) * ((( |.(f + g).| . x) |^ 1) * ( |.(f + g).| . x))) by Th10;

        

         A29: ( |.(f + g).| . x) = |.((f + g) . x).| by A13, A15, A6, A25, MESFUNC1:def 10;

         |.((f + g) . x).| = |.((f . x) + (g . x)).| by A14, A15, A6, A25, MESFUNC1:def 3;

        then (((1 / 4) (#) ( |.(f + g).| |^ 2)) . x) = ((1 / 4) * ( |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|)) by A29, A28, Th9;

        then

         A30: (((1 / 4) (#) ( |.(f + g).| |^ 2)) . x) = ((1 / 4) * ( |.(c1 + c2) qua Complex.| * |.(c1 + c2) qua Complex.|)) by A27, EXTREAL1: 1;

        ( |.(c1 - c2) qua Complex.| * |.(c1 - c2) qua Complex.|) = ( |.(c1 - c2) qua Complex.| ^2 );

        then

         A31: ( |.(c1 - c2) qua Complex.| * |.(c1 - c2) qua Complex.|) = ((c1 - c2) ^2 ) by COMPLEX1: 75;

        (((1 / 4) (#) ( |.(f - g).| |^ 2)) . x) = ((1 / 4) * (( |.(f - g).| |^ 2) . x)) by A10, A6, A12, A25, MESFUNC1:def 6;

        then (((1 / 4) (#) ( |.(f - g).| |^ 2)) . x) = ((1 / 4) * (( |.(f - g).| . x) |^ (1 + 1))) by A10, A6, A25, Def4;

        then

         A32: (((1 / 4) (#) ( |.(f - g).| |^ 2)) . x) = ((1 / 4) * ((( |.(f - g).| . x) |^ 1) * ( |.(f - g).| . x))) by Th10;

        ((f . x) - (g . x)) = (c1 - c2) by SUPINF_2: 3;

        then |.((f . x) - (g . x)).| = |.(c1 - c2) qua Complex.| by EXTREAL1: 12;

        then

         A33: ( |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|) = ( |.(c1 - c2) qua Complex.| * |.(c1 - c2) qua Complex.|) by EXTREAL1: 1;

        

         A34: ( |.(f - g).| . x) = |.((f - g) . x).| by A8, A10, A6, A25, MESFUNC1:def 10;

         |.((f - g) . x).| = |.((f . x) - (g . x)).| by A9, A10, A6, A25, MESFUNC1:def 4;

        then (((1 / 4) (#) ( |.(f - g).| |^ 2)) . x) = ((1 / 4) * ( |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|)) by A34, A32, Th9;

        then

         A35: (((1 / 4) (#) ( |.(f - g).| |^ 2)) . x) = ((1 / 4) * ( |.(c1 - c2) qua Complex.| * |.(c1 - c2) qua Complex.|)) by A33, EXTREAL1: 1;

        ( |.(c1 + c2) qua Complex.| * |.(c1 + c2) qua Complex.|) = ( |.(c1 + c2) qua Complex.| ^2 );

        then ( |.(c1 + c2) qua Complex.| * |.(c1 + c2) qua Complex.|) = ((c1 + c2) ^2 ) by COMPLEX1: 75;

        

        then ((((1 / 4) (#) ( |.(f + g).| |^ 2)) . x) - (((1 / 4) (#) ( |.(f - g).| |^ 2)) . x)) = (((1 / 4) * (((c1 ^2 ) + ((2 * c1) * c2)) + (c2 ^2 ))) - ((1 / 4) * (((c1 ^2 ) - ((2 * c1) * c2)) + (c2 ^2 )))) by A30, A35, A31, SUPINF_2: 3

        .= (c1 * c2)

        .= ((f . x) * (g . x)) by EXTREAL1: 1

        .= ((f (#) g) . x) by A25, MESFUNC1:def 5;

        hence thesis by A15, A10, A6, A7, A12, A24, A25, MESFUNC1:def 4;

      end;

      then

       A36: (f (#) g) = (((1 / 4) (#) ( |.(f + g).| |^ 2)) - ((1 / 4) (#) ( |.(f - g).| |^ 2))) by A15, A10, A6, A7, A12, A24, PARTFUN1: 5;

      

       A37: ( dom ( |.(f - g).| |^ 2)) c= ( dom f) by A10, XBOOLE_1: 17;

      for x be Element of X st x in ( dom ( |.(f - g).| |^ 2)) holds |.(( |.(f - g).| |^ 2) . x).| < +infty

      proof

        let x be Element of X;

        assume

         A38: x in ( dom ( |.(f - g).| |^ 2));

        then

         A39: |.(g . x).| < +infty by A3, A11, MESFUNC2:def 1;

         |.(f . x).| < +infty by A2, A37, A38, MESFUNC2:def 1;

        then

        reconsider c1 = (f . x), c2 = (g . x) as Element of REAL by A39, EXTREAL1: 41;

        ((f . x) - (g . x)) = (c1 - c2) by SUPINF_2: 3;

        then |.((f . x) - (g . x)).| = |.(c1 - c2) qua Complex.| by EXTREAL1: 12;

        then

         A40: ( |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|) = ( |.(c1 - c2) qua Complex.| * |.(c1 - c2) qua Complex.|) by EXTREAL1: 1;

        (( |.(f - g).| |^ 2) . x) = (( |.(f - g).| . x) |^ (1 + 1)) by A38, Def4;

        then

         A41: (( |.(f - g).| |^ 2) . x) = ((( |.(f - g).| . x) |^ 1) * ( |.(f - g).| . x)) by Th10;

        ( |.(f - g).| . x) = |.((f - g) . x).| by A8, A38, MESFUNC1:def 10;

        then ( |.(f - g).| . x) = |.((f . x) - (g . x)).| by A9, A38, MESFUNC1:def 4;

        

        then |.(( |.(f - g).| |^ 2) . x).| = |.( |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|).| by A41, Th9

        .= |. |.(((f . x) - (g . x)) * ((f . x) - (g . x))).|.| by EXTREAL1: 19

        .= |.(((f . x) - (g . x)) * ((f . x) - (g . x))).|

        .= ( |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|) by EXTREAL1: 19;

        hence thesis by A40, XXREAL_0: 9, XREAL_0:def 1;

      end;

      then ( |.(f - g).| |^ 2) is real-valued by MESFUNC2:def 1;

      then

       A42: ((1 / 4) (#) ( |.(f - g).| |^ 2)) is real-valued by MESFUNC2: 10;

      (f + g) is E -measurable by A2, A3, A4, A5, MESFUNC2: 7;

      then ( |.(f + g).| |^ 2) is E -measurable by A1, A14, A15, Th14;

      then

       A43: ((jj / 4) (#) ( |.(f + g).| |^ 2)) is E -measurable by A1, A15, MESFUNC5: 49;

      (f - g) is E -measurable by A1, A2, A3, A4, A5, MESFUNC2: 11, XBOOLE_1: 17;

      then ( |.(f - g).| |^ 2) is E -measurable by A1, A9, A10, Th14;

      then ((jj / 4) (#) ( |.(f - g).| |^ 2)) is E -measurable by A1, A10, MESFUNC5: 49;

      hence thesis by A1, A10, A12, A23, A42, A36, A43, MESFUNC2: 11;

    end;

    theorem :: MESFUNC7:16

    

     Th16: ( rng f) is real-bounded implies f is real-valued

    proof

      assume

       A1: ( rng f) is real-bounded;

      then ( rng f) is bounded_above by XXREAL_2:def 11;

      then

      consider UB be Real such that

       A2: UB is UpperBound of ( rng f) by XXREAL_2:def 10;

      

       A3: UB in REAL by XREAL_0:def 1;

      ( rng f) is bounded_below by A1, XXREAL_2:def 11;

      then

      consider LB be Real such that

       A4: LB is LowerBound of ( rng f) by XXREAL_2:def 9;

      

       A5: LB in REAL by XREAL_0:def 1;

      now

        let x be Element of X;

        assume x in ( dom f);

        then

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

        then LB <= (f . x) by A4, XXREAL_2:def 2;

        then -infty < (f . x) by A5, XXREAL_0: 2, XXREAL_0: 12;

        then

         A7: ( - +infty ) < (f . x) by XXREAL_3: 23;

        (f . x) <= UB by A2, A6, XXREAL_2:def 1;

        then (f . x) < +infty by A3, XXREAL_0: 2, XXREAL_0: 9;

        hence |.(f . x).| < +infty by A7, EXTREAL1: 22;

      end;

      hence thesis by MESFUNC2:def 1;

    end;

    ::$Notion-Name

    theorem :: MESFUNC7:17

    for M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL , E be Element of S, F be non empty Subset of ExtREAL st (( dom f) /\ ( dom g)) = E & ( rng f) = F & g is real-valued & f is E -measurable & ( rng f) is real-bounded & g is_integrable_on M holds ((f (#) g) | E) is_integrable_on M & ex c be Element of REAL st c >= ( inf F) & c <= ( sup F) & ( Integral (M,((f (#) |.g.|) | E))) = (c * ( Integral (M,( |.g.| | E))))

    proof

      let M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL , E be Element of S, F be non empty Subset of ExtREAL ;

      assume that

       A1: (( dom f) /\ ( dom g)) = E and

       A2: ( rng f) = F and

       A3: g is real-valued and

       A4: f is E -measurable and

       A5: ( rng f) is real-bounded and

       A6: g is_integrable_on M;

      

       A7: ( dom ((f (#) |.g.|) | E)) = (( dom (f (#) |.g.|)) /\ E) by RELAT_1: 61;

      

       A8: ( rng f) is Subset of REAL by A5, Th16, MESFUNC2: 32;

      then not +infty in ( rng f);

      then

       A9: ( rng f) <> { +infty } by TARSKI:def 1;

      

       A10: ( rng f) is bounded_above by A5, XXREAL_2:def 11;

       not -infty in ( rng f) by A8;

      then

       A11: ( rng f) <> { -infty } by TARSKI:def 1;

      ( rng f) is bounded_below by A5, XXREAL_2:def 11;

      then

      reconsider k0 = ( inf F), l0 = ( sup F) as Element of REAL by A2, A10, A9, A11, XXREAL_2: 57, XXREAL_2: 58;

      

       A12: |.( sup F).| = |.l0 qua Complex.| by EXTREAL1: 12;

       |.( inf F).| = |.k0 qua Complex.| by EXTREAL1: 12;

      then

      reconsider k1 = |.( inf F).|, l1 = |.( sup F).| as Real by A12;

      

       A13: E c= ( dom f) by A1, XBOOLE_1: 17;

      

       A14: ( sup F) is UpperBound of ( rng f) by A2, XXREAL_2:def 3;

      

       A15: E c= ( dom g) by A1, XBOOLE_1: 17;

      then

       A16: E c= ( dom |.g.|) by MESFUNC1:def 10;

      

       A17: ( dom |.g.|) = ( dom g) by MESFUNC1:def 10;

      for x be Element of X st x in ( dom |.g.|) holds |.( |.g.| . x).| < +infty

      proof

        let x be Element of X;

        assume

         A18: x in ( dom |.g.|);

        then |.( |.g.| . x).| = |. |.(g . x).|.| by MESFUNC1:def 10;

        then |.( |.g.| . x).| = |.(g . x).|;

        hence thesis by A3, A17, A18, MESFUNC2:def 1;

      end;

      then

       A19: |.g.| is real-valued by MESFUNC2:def 1;

      

       A20: f is real-valued by A5, Th16;

      consider E1 be Element of S such that

       A21: E1 = ( dom g) and

       A22: g is E1 -measurable by A6;

      

       A23: E1 = ( dom |.g.|) by A21, MESFUNC1:def 10;

       |.g.| is E1 -measurable by A21, A22, MESFUNC2: 27;

      then

       A24: |.g.| is E -measurable by A1, A21, MESFUNC1: 30, XBOOLE_1: 17;

      (( dom f) /\ ( dom |.g.|)) = E by A1, MESFUNC1:def 10;

      then

       A25: (f (#) |.g.|) is E -measurable by A4, A24, A20, A19, Th15;

      

       A26: |.g.| is_integrable_on M by A6, MESFUNC5: 100;

      then

       A27: ( |.g.| | E) is_integrable_on M by MESFUNC5: 97;

      

       A28: ( dom (f (#) |.g.|)) = (( dom f) /\ ( dom |.g.|)) by MESFUNC1:def 5;

      then

       A29: ( dom (f (#) |.g.|)) = E by A1, MESFUNC1:def 10;

      

       A30: ( dom (k0 (#) |.g.|)) = ( dom |.g.|) by MESFUNC1:def 6;

      then

       A31: ( dom ((k0 (#) |.g.|) | E)) = E by A16, RELAT_1: 62;

      

       A32: ( inf F) is LowerBound of ( rng f) by A2, XXREAL_2:def 4;

      

       A33: for x be Element of X st x in E holds (( inf F) * |.(g . x).|) <= ((f . x) * |.(g . x).|) & ((f . x) * |.(g . x).|) <= (( sup F) * |.(g . x).|)

      proof

        let x be Element of X;

        

         A34: 0 <= |.(g . x).| by EXTREAL1: 14;

        assume

         A35: x in E;

        then

         A36: (f . x) <= ( sup F) by A13, A14, FUNCT_1: 3, XXREAL_2:def 1;

        ( inf F) <= (f . x) by A13, A32, A35, FUNCT_1: 3, XXREAL_2:def 2;

        hence thesis by A36, A34, XXREAL_3: 71;

      end;

      for x be Element of X st x in ( dom ((k0 (#) |.g.|) | E)) holds (((k0 (#) |.g.|) | E) . x) <= (((f (#) |.g.|) | E) . x)

      proof

        let x be Element of X;

        assume

         A37: x in ( dom ((k0 (#) |.g.|) | E));

        then

         A38: (((k0 (#) |.g.|) | E) . x) = ((k0 (#) |.g.|) . x) by FUNCT_1: 47;

        ((f (#) |.g.|) . x) = ((f . x) * ( |.g.| . x)) by A29, A31, A37, MESFUNC1:def 5;

        then

         A39: ((f (#) |.g.|) . x) = ((f . x) * |.(g . x).|) by A16, A31, A37, MESFUNC1:def 10;

        ((k0 (#) |.g.|) . x) = (k0 * ( |.g.| . x)) by A16, A30, A31, A37, MESFUNC1:def 6;

        then ((k0 (#) |.g.|) . x) = (k0 * |.(g . x).|) by A16, A31, A37, MESFUNC1:def 10;

        then ((k0 (#) |.g.|) . x) <= ((f (#) |.g.|) . x) by A33, A31, A37, A39;

        hence thesis by A29, A7, A31, A37, A38, FUNCT_1: 47;

      end;

      then

       A40: (((f (#) |.g.|) | E) - ((k0 (#) |.g.|) | E)) is nonnegative by Th1;

      

       A41: ( dom (l0 (#) |.g.|)) = ( dom |.g.|) by MESFUNC1:def 6;

      then

       A42: ( dom ((l0 (#) |.g.|) | E)) = E by A16, RELAT_1: 62;

      

       A43: ( dom (f (#) g)) = E by A1, MESFUNC1:def 5;

      then

       A44: ( dom ((f (#) g) | E)) = E by RELAT_1: 62;

      then

       A45: ( dom |.((f (#) g) | E).|) = E by MESFUNC1:def 10;

      

       A46: for x be Element of X st x in ( dom ((f (#) |.g.|) | E)) holds |.(((f (#) |.g.|) | E) . x).| <= ( |.((f (#) g) | E).| . x)

      proof

        let x be Element of X;

        assume

         A47: x in ( dom ((f (#) |.g.|) | E));

        then

         A48: (((f (#) |.g.|) | E) . x) = ((f (#) |.g.|) . x) by FUNCT_1: 47;

         |.((f (#) |.g.|) . x).| = |.((f . x) * ( |.g.| . x)).| by A29, A7, A47, MESFUNC1:def 5

        .= |.((f . x) * |.(g . x).|).| by A1, A17, A15, A28, A7, A47, MESFUNC1:def 10

        .= ( |.(f . x).| * |. |.(g . x).|.|) by EXTREAL1: 19

        .= ( |.(f . x).| * |.(g . x).|);

        then

         A49: |.((f (#) |.g.|) . x).| = |.((f . x) * (g . x)).| by EXTREAL1: 19;

        ( dom |.(f (#) g).|) = E by A43, MESFUNC1:def 10;

        then

         A50: ( |.(f (#) g).| . x) = |.((f (#) g) . x).| by A29, A7, A47, MESFUNC1:def 10;

         |.(((f (#) g) | E) . x).| = |.((f (#) g) . x).| by A44, A29, A7, A47, FUNCT_1: 47;

        then ( |.((f (#) g) | E).| . x) = ( |.(f (#) g).| . x) by A45, A29, A7, A47, A50, MESFUNC1:def 10;

        hence thesis by A43, A29, A7, A47, A49, A50, A48, MESFUNC1:def 5;

      end;

      ( Integral (M,((l0 (#) |.g.|) | E))) = ( Integral (M,(l0 (#) ( |.g.| | E)))) by Th2;

      then

       A51: ( Integral (M,((l0 (#) |.g.|) | E))) = (l0 * ( Integral (M,( |.g.| | E)))) by A27, MESFUNC5: 110;

      

       A52: (( dom (f (#) g)) /\ E) = E by A43;

      g is E -measurable by A1, A21, A22, MESFUNC1: 30, XBOOLE_1: 17;

      then (f (#) g) is E -measurable by A1, A3, A4, A20, Th15;

      then

       A53: ((f (#) g) | E) is E -measurable by A52, MESFUNC5: 42;

      

       A54: for x be Element of X st x in E holds |.(f . x).| <= ( |.( inf F).| + |.( sup F).|)

      proof

         0 <= |.k0 qua Complex.| by COMPLEX1: 46;

        then

         A55: (l0 + 0 ) <= (l0 + |.k0 qua Complex.|) by XREAL_1: 6;

        l0 <= |.l0 qua Complex.| by COMPLEX1: 76;

        then (l0 + |.k0 qua Complex.|) <= ( |.l0 qua Complex.| + |.k0 qua Complex.|) by XREAL_1: 6;

        then

         A56: l0 <= ( |.l0 qua Complex.| + |.k0 qua Complex.|) by A55, XXREAL_0: 2;

         0 <= |.l0 qua Complex.| by COMPLEX1: 46;

        then

         A57: (( - |.k0 qua Complex.|) - |.l0 qua Complex.|) <= (( - |.k0 qua Complex.|) - 0 ) by XREAL_1: 10;

        ( - |.k0 qua Complex.|) <= k0 by COMPLEX1: 76;

        then

         A58: (( - |.k0 qua Complex.|) - |.l0 qua Complex.|) <= k0 by A57, XXREAL_0: 2;

        let x be Element of X;

        

         A59: |.k0 qua Complex.| = |.( inf F).| by EXTREAL1: 12;

        assume

         A60: x in E;

        then (f . x) in ( rng f) by A13, FUNCT_1: 3;

        then

        reconsider fx = (f . x) as Real by A8;

        

         A61: |.l0 qua Complex.| = |.( sup F).| by EXTREAL1: 12;

        fx <= l0 by A13, A14, A60, FUNCT_1: 3, XXREAL_2:def 1;

        then

         A62: fx <= ( |.k0 qua Complex.| + |.l0 qua Complex.|) by A56, XXREAL_0: 2;

        k0 <= fx by A13, A32, A60, FUNCT_1: 3, XXREAL_2:def 2;

        then ( - ( |.k0 qua Complex.| + |.l0 qua Complex.|)) <= fx by A58, XXREAL_0: 2;

        then

         A63: |.fx qua Complex.| <= ( |.k0 qua Complex.| + |.l0 qua Complex.|) by A62, ABSVALUE: 5;

         |.fx qua Complex.| = |.(f . x).| by EXTREAL1: 12;

        hence thesis by A63, A59, A61, SUPINF_2: 1;

      end;

      ( dom (((k1 + l1) (#) |.g.|) | E)) = ( dom ((k1 + l1) (#) ( |.g.| | E))) by Th2;

      then ( dom (((k1 + l1) (#) |.g.|) | E)) = ( dom ( |.g.| | E)) by MESFUNC1:def 6;

      then

       A64: ( dom (((k1 + l1) (#) |.g.|) | E)) = E by A16, RELAT_1: 62;

      

       A65: ( dom ((k1 + l1) (#) |.g.|)) = ( dom |.g.|) by MESFUNC1:def 6;

      

       A66: for x be Element of X st x in ( dom ((f (#) g) | E)) holds |.(((f (#) g) | E) . x).| <= ((((k1 + l1) (#) |.g.|) | E) . x)

      proof

        let x be Element of X;

        assume

         A67: x in ( dom ((f (#) g) | E));

        then

         A68: (((f (#) g) | E) . x) = ((f (#) g) . x) by FUNCT_1: 47;

        ( dom (f | E)) = E by A1, RELAT_1: 62, XBOOLE_1: 17;

        then

         A69: ((f | E) . x) = (f . x) by A44, A67, FUNCT_1: 47;

        ( dom (g | E)) = E by A1, RELAT_1: 62, XBOOLE_1: 17;

        then

         A70: ((g | E) . x) = (g . x) by A44, A67, FUNCT_1: 47;

         0 <= |.((g | E) . x).| by EXTREAL1: 14;

        then

         A71: ( |.((f | E) . x).| * |.((g | E) . x).|) <= (( |.( inf F).| + |.( sup F).|) * |.((g | E) . x).|) by A44, A54, A67, A69, XXREAL_3: 71;

        

         A72: ((((k1 + l1) (#) |.g.|) | E) . x) = (((k1 + l1) (#) |.g.|) . x) by A44, A64, A67, FUNCT_1: 47;

         |.((f (#) g) . x).| = |.((f . x) * (g . x)).| by A43, A44, A67, MESFUNC1:def 5;

        then

         A73: |.(((f (#) g) | E) . x).| = ( |.((f | E) . x).| * |.((g | E) . x).|) by A68, A69, A70, EXTREAL1: 19;

        (((k1 + l1) (#) |.g.|) . x) = ((k1 + l1) * ( |.g.| . x)) by A16, A44, A65, A67, MESFUNC1:def 6;

        then ((((k1 + l1) (#) |.g.|) | E) . x) = ((k1 + l1) * |.((g | E) . x).|) by A16, A44, A67, A70, A72, MESFUNC1:def 10;

        hence thesis by A71, A73, SUPINF_2: 1;

      end;

      ((k1 + l1) (#) |.g.|) is_integrable_on M by A26, MESFUNC5: 110;

      then

       A74: (((k1 + l1) (#) |.g.|) | E) is_integrable_on M by MESFUNC5: 97;

      then ((f (#) g) | E) is_integrable_on M by A44, A64, A53, A66, MESFUNC5: 102;

      then

       A75: |.((f (#) g) | E).| is_integrable_on M by MESFUNC5: 100;

      (( dom (f (#) |.g.|)) /\ E) = E by A29;

      then ((f (#) |.g.|) | E) is E -measurable by A25, MESFUNC5: 42;

      then

       A76: ((f (#) |.g.|) | E) is_integrable_on M by A45, A29, A7, A75, A46, MESFUNC5: 102;

      then

       A77: -infty < ( Integral (M,((f (#) |.g.|) | E))) by MESFUNC5: 96;

      (k0 (#) |.g.|) is_integrable_on M by A26, MESFUNC5: 110;

      then ((k0 (#) |.g.|) | E) is_integrable_on M by MESFUNC5: 97;

      then

      consider V1 be Element of S such that

       A78: V1 = (( dom ((k0 (#) |.g.|) | E)) /\ ( dom ((f (#) |.g.|) | E))) and

       A79: ( Integral (M,(((k0 (#) |.g.|) | E) | V1))) <= ( Integral (M,(((f (#) |.g.|) | E) | V1))) by A76, A40, Th3;

      

       A80: (((f (#) |.g.|) | E) | V1) = ((f (#) |.g.|) | E) by A29, A7, A31, A78, RELAT_1: 68;

      

       A81: ( dom (f (#) |.g.|)) c= ( dom (l0 (#) |.g.|)) by A28, A41, XBOOLE_1: 17;

      for x be Element of X st x in ( dom ((f (#) |.g.|) | E)) holds (((f (#) |.g.|) | E) . x) <= (((l0 (#) |.g.|) | E) . x)

      proof

        let x be Element of X;

        assume

         A82: x in ( dom ((f (#) |.g.|) | E));

        then

         A83: (((f (#) |.g.|) | E) . x) = ((f (#) |.g.|) . x) by FUNCT_1: 47;

        ((f (#) |.g.|) . x) = ((f . x) * ( |.g.| . x)) by A29, A7, A82, MESFUNC1:def 5;

        then

         A84: ((f (#) |.g.|) . x) = ((f . x) * |.(g . x).|) by A16, A29, A7, A82, MESFUNC1:def 10;

        ((l0 (#) |.g.|) . x) = (l0 * ( |.g.| . x)) by A29, A7, A81, A82, MESFUNC1:def 6;

        then ((l0 (#) |.g.|) . x) = (l0 * |.(g . x).|) by A16, A29, A7, A82, MESFUNC1:def 10;

        then ((f (#) |.g.|) . x) <= ((l0 (#) |.g.|) . x) by A29, A7, A33, A82, A84;

        hence thesis by A29, A7, A42, A82, A83, FUNCT_1: 47;

      end;

      then

       A85: (((l0 (#) |.g.|) | E) - ((f (#) |.g.|) | E)) is nonnegative by Th1;

      ( Integral (M,((k0 (#) |.g.|) | E))) = ( Integral (M,(k0 (#) ( |.g.| | E)))) by Th2;

      then

       A86: ( Integral (M,((k0 (#) |.g.|) | E))) = (k0 * ( Integral (M,( |.g.| | E)))) by A27, MESFUNC5: 110;

      (l0 (#) |.g.|) is_integrable_on M by A26, MESFUNC5: 110;

      then ((l0 (#) |.g.|) | E) is_integrable_on M by MESFUNC5: 97;

      then

      consider V2 be Element of S such that

       A87: V2 = (( dom ((l0 (#) |.g.|) | E)) /\ ( dom ((f (#) |.g.|) | E))) and

       A88: ( Integral (M,(((f (#) |.g.|) | E) | V2))) <= ( Integral (M,(((l0 (#) |.g.|) | E) | V2))) by A76, A85, Th3;

      

       A89: (((f (#) |.g.|) | E) | V2) = ((f (#) |.g.|) | E) by A29, A7, A42, A87, RELAT_1: 68;

      

       A90: (((l0 (#) |.g.|) | E) | V2) = ((l0 (#) |.g.|) | E) by A29, A7, A42, A87, RELAT_1: 68;

      

       A91: ( Integral (M,((f (#) |.g.|) | E))) < +infty by A76, MESFUNC5: 96;

      

       A92: (((k0 (#) |.g.|) | E) | V1) = ((k0 (#) |.g.|) | E) by A29, A7, A31, A78, RELAT_1: 68;

      ex c be Element of REAL st c >= ( inf F) & c <= ( sup F) & ( Integral (M,((f (#) |.g.|) | E))) = (c * ( Integral (M,( |.g.| | E))))

      proof

        per cases ;

          suppose

           A93: ( Integral (M,( |.g.| | E))) <> 0. ;

          reconsider c3 = ( Integral (M,((f (#) |.g.|) | E))) as Element of REAL by A77, A91, XXREAL_0: 14;

          set c2 = (( Integral (M,((f (#) |.g.|) | E))) / ( Integral (M,( |.g.| | E))));

          

           A94: ( Integral (M,( |.g.| | E))) < +infty by A27, MESFUNC5: 96;

          

           A95: -infty < ( Integral (M,( |.g.| | E))) by A27, MESFUNC5: 96;

          then

          reconsider c1 = ( Integral (M,( |.g.| | E))) as Element of REAL by A94, XXREAL_0: 14;

          (( Integral (M,((f (#) |.g.|) | E))) / ( Integral (M,( |.g.| | E)))) = (c3 / c1);

          then

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

          

           A96: (c3 * (c1 / c1)) = (( Integral (M,((f (#) |.g.|) | E))) * (( Integral (M,( |.g.| | E))) / ( Integral (M,( |.g.| | E))))) by EXTREAL1: 1;

          (( Integral (M,( |.g.| | E))) * (( Integral (M,((f (#) |.g.|) | E))) / ( Integral (M,( |.g.| | E))))) = (c1 * (c3 / c1)) by EXTREAL1: 1;

          then

           A97: (c * ( Integral (M,( |.g.| | E)))) = ( Integral (M,((f (#) |.g.|) | E))) by A93, A96, XXREAL_3: 88;

          

           A98: ( Integral (M,( |.g.| | E))) > 0. by A21, A22, A23, A93, MESFUNC2: 27, MESFUNC5: 92;

          (( sup F) * ( Integral (M,( |.g.| | E)))) = (l0 * c1) by EXTREAL1: 1;

          then

           A99: ((( sup F) * ( Integral (M,( |.g.| | E)))) / ( Integral (M,( |.g.| | E)))) = ((l0 * c1) / c1);

          ((l0 * c1) / c1) = (l0 * (c1 / c1));

          then

           A100: ((( sup F) * ( Integral (M,( |.g.| | E)))) / ( Integral (M,( |.g.| | E)))) = (( sup F) * (( Integral (M,( |.g.| | E))) / ( Integral (M,( |.g.| | E))))) by A99, EXTREAL1: 1;

          (( inf F) * ( Integral (M,( |.g.| | E)))) = (k0 * c1) by EXTREAL1: 1;

          then

           A101: ((( inf F) * ( Integral (M,( |.g.| | E)))) / ( Integral (M,( |.g.| | E)))) = ((k0 * c1) / c1);

          ((k0 * c1) / c1) = (k0 * (c1 / c1));

          then

           A102: ((( inf F) * ( Integral (M,( |.g.| | E)))) / ( Integral (M,( |.g.| | E)))) = (( inf F) * (( Integral (M,( |.g.| | E))) / ( Integral (M,( |.g.| | E))))) by A101, EXTREAL1: 1;

          (( sup F) * (( Integral (M,( |.g.| | E))) / ( Integral (M,( |.g.| | E))))) = (( sup F) * 1. ) by A93, A95, A94, XXREAL_3: 78;

          then (( sup F) * (( Integral (M,( |.g.| | E))) / ( Integral (M,( |.g.| | E))))) = ( sup F) by XXREAL_3: 81;

          then

           A103: c <= ( sup F) by A51, A88, A89, A90, A98, A100, XXREAL_3: 79;

          (( inf F) * (( Integral (M,( |.g.| | E))) / ( Integral (M,( |.g.| | E))))) = (( inf F) * 1. ) by A93, A95, A94, XXREAL_3: 78;

          then (( inf F) * (( Integral (M,( |.g.| | E))) / ( Integral (M,( |.g.| | E))))) = ( inf F) by XXREAL_3: 81;

          then c >= ( inf F) by A86, A79, A92, A80, A98, A102, XXREAL_3: 79;

          hence thesis by A103, A97;

        end;

          suppose

           A104: ( Integral (M,( |.g.| | E))) = 0. ;

          then 0. <= ( Integral (M,((f (#) |.g.|) | E))) by A29, A7, A31, A86, A78, A79, A80, RELAT_1: 68;

          then

           A105: ( Integral (M,((f (#) |.g.|) | E))) = 0. by A29, A7, A42, A51, A87, A88, A89, A104, RELAT_1: 68;

          consider y be object such that

           A106: y in F by XBOOLE_0:def 1;

          reconsider y as Element of ExtREAL by A106;

          

           A107: y <= ( sup F) by A106, XXREAL_2: 4;

          ( inf F) <= y by A106, XXREAL_2: 3;

          then

           A108: k0 <= ( sup F) by A107, XXREAL_0: 2;

          (k0 * ( Integral (M,( |.g.| | E)))) = 0. by A104;

          hence thesis by A108, A105;

        end;

      end;

      hence thesis by A44, A64, A74, A53, A66, MESFUNC5: 102;

    end;

    begin

    reserve E1,E2 for Element of S;

    reserve x,A for set;

    reserve a,b for Real;

    theorem :: MESFUNC7:18

    

     Th18: ( |.f.| | A) = |.(f | A).|

    proof

      ( dom ( |.f.| | A)) = (( dom |.f.|) /\ A) by RELAT_1: 61;

      then

       A1: ( dom ( |.f.| | A)) = (( dom f) /\ A) by MESFUNC1:def 10;

      

       A2: ( dom (f | A)) = (( dom f) /\ A) by RELAT_1: 61;

      then

       A3: ( dom |.(f | A).|) = (( dom f) /\ A) by MESFUNC1:def 10;

      now

        let x be Element of X;

        assume

         A4: x in ( dom ( |.f.| | A));

        then ( |.(f | A).| . x) = |.((f | A) . x).| by A1, A3, MESFUNC1:def 10;

        then

         A5: ( |.(f | A).| . x) = |.(f . x).| by A2, A1, A4, FUNCT_1: 47;

        x in ( dom f) by A1, A4, XBOOLE_0:def 4;

        then

         A6: x in ( dom |.f.|) by MESFUNC1:def 10;

        (( |.f.| | A) . x) = ( |.f.| . x) by A4, FUNCT_1: 47;

        hence (( |.f.| | A) . x) = ( |.(f | A).| . x) by A6, A5, MESFUNC1:def 10;

      end;

      hence thesis by A1, A3, PARTFUN1: 5;

    end;

    theorem :: MESFUNC7:19

    

     Th19: ( dom ( |.f.| + |.g.|)) = (( dom f) /\ ( dom g)) & ( dom |.(f + g).|) c= ( dom |.f.|)

    proof

      set F = |.f.|;

      set G = |.g.|;

      F is without-infty by MESFUNC5: 12;

      then not -infty in ( rng F);

      then

       A1: (F " { -infty }) = {} by FUNCT_1: 72;

      G is without-infty by MESFUNC5: 12;

      then not -infty in ( rng G);

      then

       A2: (G " { -infty }) = {} by FUNCT_1: 72;

      ( dom ( |.f.| + |.g.|)) = ((( dom F) /\ ( dom G)) \ (((F " { -infty }) /\ (G " { +infty })) \/ ((F " { +infty }) /\ (G " { -infty })))) by MESFUNC1:def 3;

      then ( dom ( |.f.| + |.g.|)) = (( dom f) /\ ( dom G)) by A1, A2, MESFUNC1:def 10;

      hence ( dom ( |.f.| + |.g.|)) = (( dom f) /\ ( dom g)) by MESFUNC1:def 10;

      ( dom |.(f + g).|) = ( dom (f + g)) by MESFUNC1:def 10

      .= ((( dom f) /\ ( dom g)) \ (((f " { -infty }) /\ (g " { +infty })) \/ ((f " { +infty }) /\ (g " { -infty })))) by MESFUNC1:def 3

      .= (( dom f) /\ (( dom g) \ (((f " { -infty }) /\ (g " { +infty })) \/ ((f " { +infty }) /\ (g " { -infty }))))) by XBOOLE_1: 49;

      then ( dom |.(f + g).|) c= ( dom f) by XBOOLE_1: 17;

      hence thesis by MESFUNC1:def 10;

    end;

    theorem :: MESFUNC7:20

    

     Th20: (( |.f.| | ( dom |.(f + g).|)) + ( |.g.| | ( dom |.(f + g).|))) = (( |.f.| + |.g.|) | ( dom |.(f + g).|))

    proof

      

       A1: ( |.g.| | ( dom |.(f + g).|)) = |.(g | ( dom |.(f + g).|)).| by Th18;

      

       A2: ( dom |.(f + g).|) c= ( dom |.g.|) by Th19;

      then

       A3: ( dom |.(f + g).|) c= ( dom g) by MESFUNC1:def 10;

      ( dom (g | ( dom |.(f + g).|))) = (( dom g) /\ ( dom |.(f + g).|)) by RELAT_1: 61;

      then

       A4: ( dom (g | ( dom |.(f + g).|))) = ( dom |.(f + g).|) by A3, XBOOLE_1: 28;

      then

       A5: ( dom |.(g | ( dom |.(f + g).|)).|) = ( dom |.(f + g).|) by MESFUNC1:def 10;

      

       A6: ( dom |.(f + g).|) c= ( dom |.f.|) by Th19;

      then

       A7: ( dom |.(f + g).|) c= ( dom f) by MESFUNC1:def 10;

      then (( dom |.(f + g).|) /\ ( dom |.(f + g).|)) c= (( dom f) /\ ( dom g)) by A3, XBOOLE_1: 27;

      then

       A8: ( dom |.(f + g).|) c= ( dom ( |.f.| + |.g.|)) by Th19;

      then

       A9: ( dom (( |.f.| + |.g.|) | ( dom |.(f + g).|))) = ( dom |.(f + g).|) by RELAT_1: 62;

      ( dom (f | ( dom |.(f + g).|))) = (( dom f) /\ ( dom |.(f + g).|)) by RELAT_1: 61;

      then

       A10: ( dom (f | ( dom |.(f + g).|))) = ( dom |.(f + g).|) by A7, XBOOLE_1: 28;

      

       A11: ( |.f.| | ( dom |.(f + g).|)) = |.(f | ( dom |.(f + g).|)).| by Th18;

      

      then

       A12: ( dom (( |.f.| | ( dom |.(f + g).|)) + ( |.g.| | ( dom |.(f + g).|)))) = (( dom (f | ( dom |.(f + g).|))) /\ ( dom (g | ( dom |.(f + g).|)))) by A1, Th19

      .= ( dom |.(f + g).|) by A10, A4;

      

       A13: ( dom |.(f | ( dom |.(f + g).|)).|) = ( dom |.(f + g).|) by A10, MESFUNC1:def 10;

      now

        let x be Element of X;

        assume

         A14: x in ( dom (( |.f.| + |.g.|) | ( dom |.(f + g).|)));

        

        then

         A15: ((( |.f.| + |.g.|) | ( dom |.(f + g).|)) . x) = (( |.f.| + |.g.|) . x) by FUNCT_1: 47

        .= (( |.f.| . x) + ( |.g.| . x)) by A8, A9, A14, MESFUNC1:def 3

        .= ( |.(f . x).| + ( |.g.| . x)) by A6, A9, A14, MESFUNC1:def 10;

        

         A16: x in ( dom |.(f + g).|) by A8, A14, RELAT_1: 62;

        

        then ((( |.f.| | ( dom |.(f + g).|)) + ( |.g.| | ( dom |.(f + g).|))) . x) = ((( |.f.| | ( dom |.(f + g).|)) . x) + (( |.g.| | ( dom |.(f + g).|)) . x)) by A12, MESFUNC1:def 3

        .= ( |.((f | ( dom |.(f + g).|)) . x).| + ( |.(g | ( dom |.(f + g).|)).| . x)) by A13, A11, A1, A16, MESFUNC1:def 10

        .= ( |.((f | ( dom |.(f + g).|)) . x).| + |.((g | ( dom |.(f + g).|)) . x).|) by A5, A16, MESFUNC1:def 10

        .= ( |.(f . x).| + |.((g | ( dom |.(f + g).|)) . x).|) by A16, FUNCT_1: 49

        .= ( |.(f . x).| + |.(g . x).|) by A16, FUNCT_1: 49;

        hence ((( |.f.| + |.g.|) | ( dom |.(f + g).|)) . x) = ((( |.f.| | ( dom |.(f + g).|)) + ( |.g.| | ( dom |.(f + g).|))) . x) by A2, A9, A14, A15, MESFUNC1:def 10;

      end;

      hence thesis by A12, A8, PARTFUN1: 5, RELAT_1: 62;

    end;

    theorem :: MESFUNC7:21

    

     Th21: x in ( dom |.(f + g).|) implies ( |.(f + g).| . x) <= (( |.f.| + |.g.|) . x)

    proof

      

       A1: |.((f . x) + (g . x)).| <= ( |.(f . x).| + |.(g . x).|) by EXTREAL1: 24;

      assume

       A2: x in ( dom |.(f + g).|);

      then x in ( dom (f + g)) by MESFUNC1:def 10;

      then

       A3: |.((f + g) . x).| <= ( |.(f . x).| + |.(g . x).|) by A1, MESFUNC1:def 3;

      

       A4: ( dom |.(f + g).|) c= ( dom |.g.|) by Th19;

      then

       A5: |.(g . x).| = ( |.g.| . x) by A2, MESFUNC1:def 10;

      x in ( dom |.g.|) by A2, A4;

      then

       A6: x in ( dom g) by MESFUNC1:def 10;

      

       A7: ( dom |.(f + g).|) c= ( dom |.f.|) by Th19;

      then x in ( dom |.f.|) by A2;

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

      then x in (( dom f) /\ ( dom g)) by A6, XBOOLE_0:def 4;

      then

       A8: x in ( dom ( |.f.| + |.g.|)) by Th19;

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

      then ( |.(f . x).| + |.(g . x).|) = (( |.f.| + |.g.|) . x) by A5, A8, MESFUNC1:def 3;

      hence thesis by A2, A3, MESFUNC1:def 10;

    end;

    theorem :: MESFUNC7:22

    f is_integrable_on M & g is_integrable_on M implies ex E be Element of S st E = ( dom (f + g)) & ( Integral (M,( |.(f + g).| | E))) <= (( Integral (M,( |.f.| | E))) + ( Integral (M,( |.g.| | E))))

    proof

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      

       A3: |.g.| is_integrable_on M by A2, MESFUNC5: 100;

      

       A4: (f + g) is_integrable_on M by A1, A2, MESFUNC5: 108;

      

       A5: |.(f + g).| is_integrable_on M by A4, MESFUNC5: 100;

      for x be Element of X st x in ( dom |.(f + g).|) holds ( |.(f + g).| . x) <= (( |.f.| + |.g.|) . x) by Th21;

      then

       A6: (( |.f.| + |.g.|) - |.(f + g).|) is nonnegative by Th1;

      set G = |.g.|;

      set F = |.f.|;

      

       A7: ( dom |.(f + g).|) = ( dom (f + g)) by MESFUNC1:def 10

      .= ((( dom f) /\ ( dom g)) \ (((f " { -infty }) /\ (g " { +infty })) \/ ((f " { +infty }) /\ (g " { -infty })))) by MESFUNC1:def 3;

      

       A8: |.f.| is_integrable_on M by A1, MESFUNC5: 100;

      then ( |.f.| + |.g.|) is_integrable_on M by A3, MESFUNC5: 108;

      then

      consider E be Element of S such that

       A9: E = (( dom ( |.f.| + |.g.|)) /\ ( dom |.(f + g).|)) and

       A10: ( Integral (M,( |.(f + g).| | E))) <= ( Integral (M,(( |.f.| + |.g.|) | E))) by A5, A6, Th3;

      

       A11: (G | E) is_integrable_on M by A3, MESFUNC5: 97;

      (F | E) is_integrable_on M by A8, MESFUNC5: 97;

      then

      consider E1 be Element of S such that

       A12: E1 = (( dom (F | E)) /\ ( dom (G | E))) and

       A13: ( Integral (M,((F | E) + (G | E)))) = (( Integral (M,((F | E) | E1))) + ( Integral (M,((G | E) | E1)))) by A11, MESFUNC5: 109;

      take E;

      ( dom (G | E)) = (( dom G) /\ E) by RELAT_1: 61;

      then

       A14: ( dom (G | E)) = (( dom g) /\ E) by MESFUNC1:def 10;

      

       A15: ( dom ( |.f.| + |.g.|)) = (( dom f) /\ ( dom g)) by Th19;

      then

       A16: E = ( dom |.(f + g).|) by A9, A7, XBOOLE_1: 28, XBOOLE_1: 36;

      ( dom (F | E)) = (( dom F) /\ E) by RELAT_1: 61;

      then ( dom (F | E)) = (( dom f) /\ E) by MESFUNC1:def 10;

      then E1 = (((( dom f) /\ E) /\ E) /\ ( dom g)) by A12, A14, XBOOLE_1: 16;

      then E1 = ((( dom f) /\ (E /\ E)) /\ ( dom g)) by XBOOLE_1: 16;

      then E1 = ((( dom f) /\ ( dom g)) /\ E) by XBOOLE_1: 16;

      then

       A17: E1 = E by A9, A15, A7, XBOOLE_1: 28, XBOOLE_1: 36;

      then

       A18: ((G | E) | E1) = (G | E) by FUNCT_1: 51;

      ((F | E) | E1) = (F | E) by A17, FUNCT_1: 51;

      hence thesis by A10, A13, A16, A18, Th20, MESFUNC1:def 10;

    end;

    theorem :: MESFUNC7:23

    

     Th23: ( max+ ( chi (A,X))) = ( chi (A,X))

    proof

      

       A1: ( dom ( max+ ( chi (A,X)))) = ( dom ( chi (A,X))) by MESFUNC2:def 2;

      now

        let x be Element of X;

        

         A2: ( rng ( chi (A,X))) c= { 0 , 1} by FUNCT_3: 39;

        assume

         A3: x in ( dom ( max+ ( chi (A,X))));

        then

         A4: (( max+ ( chi (A,X))) . x) = ( max ((( chi (A,X)) . x), 0. )) by MESFUNC2:def 2;

        (( chi (A,X)) . x) in ( rng ( chi (A,X))) by A1, A3, FUNCT_1: 3;

        hence (( max+ ( chi (A,X))) . x) = (( chi (A,X)) . x) by A4, A2, XXREAL_0:def 10;

      end;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: MESFUNC7:24

    

     Th24: (M . E) < +infty implies ( chi (E,X)) is_integrable_on M & ( Integral (M,( chi (E,X)))) = (M . E) & ( Integral (M,(( chi (E,X)) | E))) = (M . E)

    proof

      reconsider XX = X as Element of S by MEASURE1: 7;

      set F = (XX \ E);

       A1:

      now

        let x be Element of X;

         A2:

        now

          assume x in E;

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

          hence ( max (( - (( chi (E,X)) . x)), 0. )) = 0. by XXREAL_0:def 10;

        end;

         A3:

        now

          assume not x in E;

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

          then ( - (( chi (E,X)) . x)) = 0 ;

          hence ( max (( - (( chi (E,X)) . x)), 0. )) = 0. ;

        end;

        assume x in ( dom ( max- ( chi (E,X))));

        hence (( max- ( chi (E,X))) . x) = 0 by A2, A3, MESFUNC2:def 3;

      end;

      

       A4: XX = ( dom ( chi (E,X))) by FUNCT_3:def 3;

      then

       A5: XX = ( dom ( max+ ( chi (E,X)))) by Th23;

      

       A6: (XX /\ F) = F by XBOOLE_1: 28;

      then

       A7: ( dom (( max+ ( chi (E,X))) | F)) = F by A5, RELAT_1: 61;

       A8:

      now

        let x be Element of X;

        assume

         A9: x in ( dom (( max+ ( chi (E,X))) | F));

        then (( chi (E,X)) . x) = 0 by A7, FUNCT_3: 37;

        then (( max+ ( chi (E,X))) . x) = 0 by Th23;

        hence ((( max+ ( chi (E,X))) | F) . x) = 0 by A9, FUNCT_1: 47;

      end;

      

       A10: ( chi (E,X)) is XX -measurable by MESFUNC2: 29;

      then

       A11: ( max+ ( chi (E,X))) is XX -measurable by Th23;

      then ( max+ ( chi (E,X))) is F -measurable by MESFUNC1: 30;

      then

       A12: ( integral+ (M,(( max+ ( chi (E,X))) | F))) = 0 by A5, A6, A7, A8, MESFUNC5: 42, MESFUNC5: 87;

      XX = ( dom ( max- ( chi (E,X)))) by A4, MESFUNC2:def 3;

      then

       A13: ( integral+ (M,( max- ( chi (E,X))))) = 0 by A4, A10, A1, MESFUNC2: 26, MESFUNC5: 87;

      

       A14: (XX /\ E) = E by XBOOLE_1: 28;

      then

       A15: ( dom (( max+ ( chi (E,X))) | E)) = E by A5, RELAT_1: 61;

      (E \/ F) = XX by A14, XBOOLE_1: 51;

      then

       A16: (( max+ ( chi (E,X))) | (E \/ F)) = ( max+ ( chi (E,X))) by A5, RELAT_1: 69;

      

       A17: for x be object st x in ( dom ( max+ ( chi (E,X)))) holds 0. <= (( max+ ( chi (E,X))) . x) by MESFUNC2: 12;

      then

       A18: ( max+ ( chi (E,X))) is nonnegative by SUPINF_2: 52;

      then ( integral+ (M,(( max+ ( chi (E,X))) | (E \/ F)))) = (( integral+ (M,(( max+ ( chi (E,X))) | E))) + ( integral+ (M,(( max+ ( chi (E,X))) | F)))) by A5, A11, MESFUNC5: 81, XBOOLE_1: 79;

      then

       A19: ( integral+ (M,( max+ ( chi (E,X))))) = ( integral+ (M,(( max+ ( chi (E,X))) | E))) by A16, A12, XXREAL_3: 4;

       A20:

      now

        let x be object;

        assume

         A21: x in ( dom (( max+ ( chi (E,X))) | E));

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

        then (( max+ ( chi (E,X))) . x) = 1 by Th23;

        hence ((( max+ ( chi (E,X))) | E) . x) = jj by A21, FUNCT_1: 47;

      end;

      then (( max+ ( chi (E,X))) | E) is_simple_func_in S by A15, MESFUNC6: 2;

      then ( integral+ (M,( max+ ( chi (E,X))))) = ( integral' (M,(( max+ ( chi (E,X))) | E))) by A18, A19, MESFUNC5: 15, MESFUNC5: 77;

      then

       A22: ( integral+ (M,( max+ ( chi (E,X))))) = (jj * (M . ( dom (( max+ ( chi (E,X))) | E)))) by A15, A20, MESFUNC5: 104;

      ( max+ ( chi (E,X))) is E -measurable by A11, MESFUNC1: 30;

      then (( max+ ( chi (E,X))) | E) is E -measurable by A5, A14, MESFUNC5: 42;

      then

       A23: (( chi (E,X)) | E) is E -measurable by Th23;

      (( max+ ( chi (E,X))) | E) is nonnegative by A17, MESFUNC5: 15, SUPINF_2: 52;

      then

       A24: (( chi (E,X)) | E) is nonnegative by Th23;

      E = ( dom (( chi (E,X)) | E)) by A15, Th23;

      then

       A25: ( Integral (M,(( chi (E,X)) | E))) = ( integral+ (M,(( chi (E,X)) | E))) by A23, A24, MESFUNC5: 88;

      assume (M . E) < +infty ;

      then ( integral+ (M,( max+ ( chi (E,X))))) < +infty by A15, A22, XXREAL_3: 81;

      hence ( chi (E,X)) is_integrable_on M by A4, A10, A13;

      ( Integral (M,( chi (E,X)))) = (1 * (M . E)) by A15, A22, A13, XXREAL_3: 15;

      hence ( Integral (M,( chi (E,X)))) = (M . E) by XXREAL_3: 81;

      (( chi (E,X)) | E) = (( max+ ( chi (E,X))) | E) by Th23;

      hence thesis by A15, A19, A22, A25, XXREAL_3: 81;

    end;

    theorem :: MESFUNC7:25

    

     Th25: (M . (E1 /\ E2)) < +infty implies ( Integral (M,(( chi (E1,X)) | E2))) = (M . (E1 /\ E2))

    proof

      reconsider XX = X as Element of S by MEASURE1: 7;

      

       A1: E2 = ((E1 /\ E2) \/ (E2 \ E1)) by XBOOLE_1: 51;

      set F = (E2 \ E1);

      

       A2: ( dom (( chi (E1,X)) | (E1 /\ E2))) = (( dom ( chi (E1,X))) /\ (E1 /\ E2)) by RELAT_1: 61

      .= (X /\ (E1 /\ E2)) by FUNCT_3:def 3;

      

       A3: ( dom (( chi ((E1 /\ E2),X)) | (E1 /\ E2))) = (( dom ( chi ((E1 /\ E2),X))) /\ (E1 /\ E2)) by RELAT_1: 61

      .= (X /\ (E1 /\ E2)) by FUNCT_3:def 3;

      now

        let x be Element of X;

        assume

         A4: x in ( dom (( chi (E1,X)) | (E1 /\ E2)));

        then

         A5: ((( chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x) = (( chi ((E1 /\ E2),X)) . x) by A2, A3, FUNCT_1: 47;

        

         A6: x in (E1 /\ E2) by A2, A4, XBOOLE_0:def 4;

        then

         A7: x in E1 by XBOOLE_0:def 4;

        ((( chi (E1,X)) | (E1 /\ E2)) . x) = (( chi (E1,X)) . x) by A4, FUNCT_1: 47

        .= 1 by A7, FUNCT_3:def 3;

        hence ((( chi (E1,X)) | (E1 /\ E2)) . x) = ((( chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x) by A6, A5, FUNCT_3:def 3;

      end;

      then

       A8: (( chi (E1,X)) | (E1 /\ E2)) = (( chi ((E1 /\ E2),X)) | (E1 /\ E2)) by A2, A3, PARTFUN1: 5;

      assume (M . (E1 /\ E2)) < +infty ;

      then

       A9: ( Integral (M,(( chi (E1,X)) | (E1 /\ E2)))) = (M . (E1 /\ E2)) by A8, Th24;

      

       A10: XX = ( dom ( chi (E1,X))) by FUNCT_3:def 3;

      then

       A11: F = ( dom (( chi (E1,X)) | (E2 \ E1))) by RELAT_1: 62;

      then F = (( dom ( chi (E1,X))) /\ F) by RELAT_1: 61;

      then

       A12: (( chi (E1,X)) | (E2 \ E1)) is F -measurable by MESFUNC2: 29, MESFUNC5: 42;

      now

        let x be object;

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

        then

         A13: (( chi (E1,X)) . x) in ( rng ( chi (E1,X))) by FUNCT_1: 3;

        ( rng ( chi (E1,X))) c= { 0 , 1} by FUNCT_3: 39;

        hence 0. <= (( chi (E1,X)) . x) by A13;

      end;

      then

       A14: ( chi (E1,X)) is nonnegative by SUPINF_2: 52;

      now

        let x be Element of X;

        assume

         A15: x in ( dom (( chi (E1,X)) | (E2 \ E1)));

        (E2 \ E1) c= (X \ E1) by XBOOLE_1: 33;

        then (( chi (E1,X)) . x) = 0 by A11, A15, FUNCT_3: 37;

        hence 0 = ((( chi (E1,X)) | (E2 \ E1)) . x) by A15, FUNCT_1: 47;

      end;

      then ( integral+ (M,(( chi (E1,X)) | (E2 \ E1)))) = 0 by A11, A12, MESFUNC5: 87;

      then

       A16: ( Integral (M,(( chi (E1,X)) | (E2 \ E1)))) = 0. by A14, A11, A12, MESFUNC5: 15, MESFUNC5: 88;

      ( chi (E1,X)) is XX -measurable by MESFUNC2: 29;

      then ( Integral (M,(( chi (E1,X)) | E2))) = (( Integral (M,(( chi (E1,X)) | (E1 /\ E2)))) + ( Integral (M,(( chi (E1,X)) | (E2 \ E1))))) by A10, A14, A1, MESFUNC5: 91, XBOOLE_1: 89;

      hence thesis by A9, A16, XXREAL_3: 4;

    end;

    theorem :: MESFUNC7:26

    f is_integrable_on M & E c= ( dom f) & (M . E) < +infty & (for x be Element of X st x in E holds a <= (f . x) & (f . x) <= b) implies (a * (M . E)) <= ( Integral (M,(f | E))) & ( Integral (M,(f | E))) <= (b * (M . E))

    proof

      reconsider a1 = a, b1 = b as Element of REAL by XREAL_0:def 1;

      assume that

       A1: f is_integrable_on M and

       A2: E c= ( dom f) and

       A3: (M . E) < +infty and

       A4: for x be Element of X st x in E holds a <= (f . x) & (f . x) <= b;

      set C = ( chi (E,X));

      

       A5: (f | E) is_integrable_on M by A1, MESFUNC5: 97;

      for x be Element of X st x in ( dom (a1 (#) (C | E))) holds ((a1 (#) (C | E)) . x) <= ((f | E) . x)

      proof

        let x be Element of X;

        assume

         A6: x in ( dom (a1 (#) (C | E)));

        then

         A7: x in ( dom (C | E)) by MESFUNC1:def 6;

        then x in (( dom C) /\ E) by RELAT_1: 61;

        then

         A8: x in E by XBOOLE_0:def 4;

        then a <= (f . x) by A4;

        then

         A9: a <= ((f | E) . x) by A8, FUNCT_1: 49;

        ((a1 (#) (C | E)) . x) = (a * ((C | E) . x)) by A6, MESFUNC1:def 6

        .= (a * (C . x)) by A7, FUNCT_1: 47

        .= (a * 1. ) by A8, FUNCT_3:def 3;

        hence thesis by A9, XXREAL_3: 81;

      end;

      then

       A10: ((f | E) - (a1 (#) (C | E))) is nonnegative by Th1;

      ( chi (E,X)) is_integrable_on M by A3, Th24;

      then

       A11: (C | E) is_integrable_on M by MESFUNC5: 97;

      then (a1 (#) (C | E)) is_integrable_on M by MESFUNC5: 110;

      then

      consider E1 be Element of S such that

       A12: E1 = (( dom (f | E)) /\ ( dom (a1 (#) (C | E)))) and

       A13: ( Integral (M,((a1 (#) (C | E)) | E1))) <= ( Integral (M,((f | E) | E1))) by A5, A10, Th3;

      ( dom (f | E)) = (( dom f) /\ E) by RELAT_1: 61;

      then

       A14: ( dom (f | E)) = E by A2, XBOOLE_1: 28;

      ( dom (a1 (#) (C | E))) = ( dom (C | E)) by MESFUNC1:def 6;

      then ( dom (a1 (#) (C | E))) = (( dom C) /\ E) by RELAT_1: 61;

      then ( dom (a1 (#) (C | E))) = (X /\ E) by FUNCT_3:def 3;

      then

       A15: ( dom (a1 (#) (C | E))) = E by XBOOLE_1: 28;

      then

       A16: ((f | E) | E1) = (f | E) by A12, A14, RELAT_1: 69;

      ( dom (b1 (#) (C | E))) = ( dom (C | E)) by MESFUNC1:def 6;

      then ( dom (b1 (#) (C | E))) = (( dom C) /\ E) by RELAT_1: 61;

      then ( dom (b1 (#) (C | E))) = (X /\ E) by FUNCT_3:def 3;

      then

       A17: ( dom (b1 (#) (C | E))) = E by XBOOLE_1: 28;

      for x be Element of X st x in ( dom (f | E)) holds ((f | E) . x) <= ((b1 (#) (C | E)) . x)

      proof

        let x be Element of X;

        assume

         A18: x in ( dom (f | E));

        then

         A19: x in ( dom (C | E)) by A14, A15, MESFUNC1:def 6;

        then x in (( dom C) /\ E) by RELAT_1: 61;

        then

         A20: x in E by XBOOLE_0:def 4;

        then (f . x) <= b by A4;

        then

         A21: ((f | E) . x) <= b by A20, FUNCT_1: 49;

        ((b1 (#) (C | E)) . x) = (b * ((C | E) . x)) by A14, A17, A18, MESFUNC1:def 6

        .= (b * (C . x)) by A19, FUNCT_1: 47

        .= (b * 1. ) by A20, FUNCT_3:def 3;

        hence thesis by A21, XXREAL_3: 81;

      end;

      then

       A22: ((b1 (#) (C | E)) - (f | E)) is nonnegative by Th1;

      (b1 (#) (C | E)) is_integrable_on M by A11, MESFUNC5: 110;

      then

      consider E2 be Element of S such that

       A23: E2 = (( dom (f | E)) /\ ( dom (b1 (#) (C | E)))) and

       A24: ( Integral (M,((f | E) | E2))) <= ( Integral (M,((b1 (#) (C | E)) | E2))) by A5, A22, Th3;

      

       A25: ((b1 (#) (C | E)) | E2) = (b1 (#) (C | E)) by A14, A17, A23, RELAT_1: 69;

      E = (E /\ E);

      then

       A26: ( Integral (M,(C | E))) = (M . E) by A3, Th25;

      

       A27: ((f | E) | E2) = (f | E) by A14, A17, A23, RELAT_1: 69;

      ((a1 (#) (C | E)) | E1) = (a1 (#) (C | E)) by A12, A14, A15, RELAT_1: 69;

      hence thesis by A11, A13, A24, A25, A16, A27, A26, MESFUNC5: 110;

    end;