mesfun13.miz



    begin

    reserve X for set;

    theorem :: MESFUN13:1

    

     Th15: for A be Subset of X, f be X -defined Relation holds (f | (A ` )) = (f | (( dom f) \ A))

    proof

      let A be Subset of X, f be X -defined Relation;

      (f | (A ` )) = ((f | ( dom f)) | (A ` ))

      .= (f | (( dom f) /\ (A ` ))) by RELAT_1: 71

      .= (f | (( dom f) /\ (X \ A))) by SUBSET_1:def 4

      .= (f | ((( dom f) /\ X) \ A)) by XBOOLE_1: 49;

      hence (f | (A ` )) = (f | (( dom f) \ A)) by XBOOLE_1: 28;

    end;

    theorem :: MESFUN13:2

    

     Th10: for f be PartFunc of X, ExtREAL holds ( great_eq_dom (f, +infty )) = ( eq_dom (f, +infty ))

    proof

      let f be PartFunc of X, ExtREAL ;

      now

        let x be object;

        assume x in ( great_eq_dom (f, +infty ));

        then

         A1: x in ( dom f) & +infty <= (f . x) by MESFUNC1:def 14;

        then (f . x) = +infty by XXREAL_0: 4;

        hence x in ( eq_dom (f, +infty )) by A1, MESFUNC1:def 15;

      end;

      then

       A2: ( great_eq_dom (f, +infty )) c= ( eq_dom (f, +infty ));

      now

        let x be object;

        assume x in ( eq_dom (f, +infty ));

        then x in ( dom f) & +infty = (f . x) by MESFUNC1:def 15;

        hence x in ( great_eq_dom (f, +infty )) by MESFUNC1:def 14;

      end;

      then ( eq_dom (f, +infty )) c= ( great_eq_dom (f, +infty ));

      hence ( great_eq_dom (f, +infty )) = ( eq_dom (f, +infty )) by A2;

    end;

    theorem :: MESFUN13:3

    for f be PartFunc of X, ExtREAL holds ( less_eq_dom (f, -infty )) = ( eq_dom (f, -infty ))

    proof

      let f be PartFunc of X, ExtREAL ;

      now

        let x be object;

        assume x in ( less_eq_dom (f, -infty ));

        then

         A1: x in ( dom f) & -infty >= (f . x) by MESFUNC1:def 12;

        then (f . x) = -infty by XXREAL_0: 6;

        hence x in ( eq_dom (f, -infty )) by A1, MESFUNC1:def 15;

      end;

      then

       A2: ( less_eq_dom (f, -infty )) c= ( eq_dom (f, -infty ));

      now

        let x be object;

        assume x in ( eq_dom (f, -infty ));

        then x in ( dom f) & -infty = (f . x) by MESFUNC1:def 15;

        hence x in ( less_eq_dom (f, -infty )) by MESFUNC1:def 12;

      end;

      then ( eq_dom (f, -infty )) c= ( less_eq_dom (f, -infty ));

      hence ( less_eq_dom (f, -infty )) = ( eq_dom (f, -infty )) by A2;

    end;

    theorem :: MESFUN13:4

    for f be PartFunc of X, ExtREAL , er be ExtReal holds ( great_eq_dom (f,er)) misses ( less_dom (f,er))

    proof

      let f be PartFunc of X, ExtREAL , er be ExtReal;

      now

        let x be object;

        assume x in (( great_eq_dom (f,er)) /\ ( less_dom (f,er)));

        then x in ( great_eq_dom (f,er)) & x in ( less_dom (f,er)) by XBOOLE_0:def 4;

        then (f . x) >= er & (f . x) < er by MESFUNC1:def 11, MESFUNC1:def 14;

        hence contradiction;

      end;

      hence thesis by XBOOLE_0:def 1;

    end;

    theorem :: MESFUN13:5

    for f be PartFunc of X, ExtREAL holds ( dom f) = ((( eq_dom (f, -infty )) \/ (( great_dom (f, -infty )) /\ ( less_dom (f, +infty )))) \/ ( eq_dom (f, +infty )))

    proof

      let f be PartFunc of X, ExtREAL ;

      set A1 = ( eq_dom (f, -infty )), A2 = (( great_dom (f, -infty )) /\ ( less_dom (f, +infty ))), A3 = ( eq_dom (f, +infty ));

      now

        let x be object;

        assume

         A1: x in ( dom f);

        per cases by XXREAL_0: 14;

          suppose (f . x) in REAL ;

          then (f . x) > -infty & (f . x) < +infty by XXREAL_0: 9, XXREAL_0: 12;

          then x in ( great_dom (f, -infty )) & x in ( less_dom (f, +infty )) by A1, MESFUNC1:def 11, MESFUNC1:def 13;

          then

           A2: x in A2 by XBOOLE_0:def 4;

          A2 c= (A1 \/ A2) & (A1 \/ A2) c= ((A1 \/ A2) \/ A3) by XBOOLE_1: 7;

          hence x in ((A1 \/ A2) \/ A3) by A2;

        end;

          suppose (f . x) = +infty ;

          then

           A3: x in A3 by A1, MESFUNC1:def 15;

          A3 c= ((A1 \/ A2) \/ A3) by XBOOLE_1: 7;

          hence x in ((A1 \/ A2) \/ A3) by A3;

        end;

          suppose (f . x) = -infty ;

          then

           A4: x in A1 by A1, MESFUNC1:def 15;

          A1 c= (A1 \/ A2) & (A1 \/ A2) c= ((A1 \/ A2) \/ A3) by XBOOLE_1: 7;

          hence x in ((A1 \/ A2) \/ A3) by A4;

        end;

      end;

      then

       A5: ( dom f) c= ((A1 \/ A2) \/ A3);

      now

        let x be object;

        assume x in ((A1 \/ A2) \/ A3);

        then

         A6: x in (A1 \/ A2) or x in A3 by XBOOLE_0:def 3;

        per cases by A6, XBOOLE_0:def 3;

          suppose x in A1;

          hence x in ( dom f) by MESFUNC1:def 15;

        end;

          suppose x in A2;

          then x in ( great_dom (f, -infty )) by XBOOLE_0:def 4;

          hence x in ( dom f) by MESFUNC1:def 13;

        end;

          suppose x in A3;

          hence x in ( dom f) by MESFUNC1:def 15;

        end;

      end;

      then ((A1 \/ A2) \/ A3) c= ( dom f);

      hence thesis by A5;

    end;

    reserve X,X1,X2 for non empty set;

    theorem :: MESFUN13:6

    

     Th29: for f be PartFunc of X, ExtREAL , x be Element of X holds (( max+ f) . x) <= ( |.f.| . x) & (( max- f) . x) <= ( |.f.| . x)

    proof

      let f be PartFunc of X, ExtREAL , x be Element of X;

      

       A1: ( - (f . x)) <= ( - ( - |.(f . x).|)) by XXREAL_3: 38, EXTREAL1: 20;

      ((( max+ f) . x) = (f . x) or (( max+ f) . x) = 0 ) & ((( max- f) . x) = ( - (f . x)) or (( max- f) . x) = 0 ) by MESFUNC2: 18;

      then

       A2: (( max+ f) . x) <= |.(f . x).| & (( max- f) . x) <= |.(f . x).| by A1, EXTREAL1: 14, EXTREAL1: 20;

      per cases ;

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

        hence (( max+ f) . x) <= ( |.f.| . x) & (( max- f) . x) <= ( |.f.| . x) by A2, MESFUNC1:def 10;

      end;

        suppose

         A3: not x in ( dom |.f.|);

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

        then (f . x) = 0 & ( |.f.| . x) = 0 by A3, FUNCT_1:def 2;

        hence (( max+ f) . x) <= ( |.f.| . x) & (( max- f) . x) <= ( |.f.| . x) by A1, MESFUNC2: 18;

      end;

    end;

    theorem :: MESFUN13:7

    

     Th27: for f be PartFunc of [:X1, X2:], ExtREAL , x be Element of X1, y be Element of X2 holds ( ProjPMap1 ( |.f.|,x)) = |.( ProjPMap1 (f,x)).| & ( ProjPMap2 ( |.f.|,y)) = |.( ProjPMap2 (f,y)).|

    proof

      let f be PartFunc of [:X1, X2:], ExtREAL , x be Element of X1, y be Element of X2;

      

       A1: |.f.| = (( max+ f) + ( max- f)) by MESFUNC2: 24;

      

      then ( ProjPMap1 ( |.f.|,x)) = (( ProjPMap1 (( max+ f),x)) + ( ProjPMap1 (( max- f),x))) by MESFUN12: 44

      .= (( max+ ( ProjPMap1 (f,x))) + ( ProjPMap1 (( max- f),x))) by MESFUN12: 45

      .= (( max+ ( ProjPMap1 (f,x))) + ( max- ( ProjPMap1 (f,x)))) by MESFUN12: 45;

      hence ( ProjPMap1 ( |.f.|,x)) = |.( ProjPMap1 (f,x)).| by MESFUNC2: 24;

      ( ProjPMap2 ( |.f.|,y)) = (( ProjPMap2 (( max+ f),y)) + ( ProjPMap2 (( max- f),y))) by A1, MESFUN12: 44

      .= (( max+ ( ProjPMap2 (f,y))) + ( ProjPMap2 (( max- f),y))) by MESFUN12: 46

      .= (( max+ ( ProjPMap2 (f,y))) + ( max- ( ProjPMap2 (f,y)))) by MESFUN12: 46;

      hence ( ProjPMap2 ( |.f.|,y)) = |.( ProjPMap2 (f,y)).| by MESFUNC2: 24;

    end;

    begin

    reserve S for SigmaField of X;

    reserve S1 for SigmaField of X1;

    reserve S2 for SigmaField of X2;

    reserve M for sigma_Measure of S;

    reserve M1 for sigma_Measure of S1;

    reserve M2 for sigma_Measure of S2;

    registration

      let X be non empty set, S be SigmaField of X, E be Element of S;

      cluster E -measurable for PartFunc of X, ExtREAL ;

      existence

      proof

        reconsider f = ( chi (E,X)) as PartFunc of X, ExtREAL ;

        take f;

        thus f is E -measurable by MESFUNC2: 29;

      end;

    end

    theorem :: MESFUN13:8

    

     Th9: for E be Element of S, f be E -measurable PartFunc of X, ExtREAL st ( dom f) = E holds ( eq_dom (f, +infty )) in S & ( eq_dom (f, -infty )) in S

    proof

      let E be Element of S, f be E -measurable PartFunc of X, ExtREAL ;

      assume

       A1: ( dom f) = E;

      then

       A2: ( eq_dom (f, +infty )) c= E & ( eq_dom (f, -infty )) c= E by MESFUNC1:def 15;

      (E /\ ( eq_dom (f, +infty ))) in S & (E /\ ( eq_dom (f, -infty ))) in S by A1, MESFUNC1: 33, MESFUNC1: 34;

      hence thesis by A2, XBOOLE_1: 28;

    end;

    theorem :: MESFUN13:9

    

     Th1: for E be Element of ( sigma ( measurable_rectangles (S1,S2))), f be E -measurable PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & ( dom f) = E holds ( Integral (M1,( Integral2 (M2, |.f.|)))) = ( Integral (( Prod_Measure (M1,M2)), |.f.|)) & ( Integral (M2,( Integral1 (M1, |.f.|)))) = ( Integral (( Prod_Measure (M1,M2)), |.f.|))

    proof

      let E be Element of ( sigma ( measurable_rectangles (S1,S2))), f be E -measurable PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: ( dom f) = E;

      E = ( dom |.f.|) & |.f.| is E -measurable by A3, MESFUNC1:def 10, MESFUNC2: 27;

      hence thesis by A1, A2, MESFUN12: 84;

    end;

    

     Lm1: for f be PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) holds ( Integral (M1,( Integral2 (M2, |.f.|)))) < +infty & ( Integral (M2,( Integral1 (M1, |.f.|)))) < +infty

    proof

      let f be PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: f is_integrable_on ( Prod_Measure (M1,M2));

      consider E be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A4: E = ( dom f) & f is E -measurable by A3, MESFUNC5:def 17;

      

       A5: |.f.| is_integrable_on ( Prod_Measure (M1,M2)) by A3, A4, MESFUNC5: 100;

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

      

      then ( Integral (( Prod_Measure (M1,M2)), |.f.|)) = ( integral+ (( Prod_Measure (M1,M2)), |.f.|)) by A4, MESFUNC2: 27, MESFUNC5: 88

      .= ( integral+ (( Prod_Measure (M1,M2)),( max+ |.f.|))) by MESFUN11: 31;

      then ( Integral (( Prod_Measure (M1,M2)), |.f.|)) < +infty by A5, MESFUNC5:def 17;

      hence thesis by A1, A2, A4, Th1;

    end;

    

     Lm2: for E be Element of ( sigma ( measurable_rectangles (S1,S2))), f be E -measurable PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & E = ( dom f) & (( Integral (M2,( Integral1 (M1, |.f.|)))) < +infty or ( Integral (M1,( Integral2 (M2, |.f.|)))) < +infty ) holds f is_integrable_on ( Prod_Measure (M1,M2))

    proof

      let E be Element of ( sigma ( measurable_rectangles (S1,S2))), f be E -measurable PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: E = ( dom f);

      set M = ( Prod_Measure (M1,M2));

      

       A5: E = ( dom |.f.|) by A3, MESFUNC1:def 10;

      then

       A6: E = ( dom ( max- |.f.|)) by MESFUNC2:def 3;

      

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

      assume ( Integral (M2,( Integral1 (M1, |.f.|)))) < +infty or ( Integral (M1,( Integral2 (M2, |.f.|)))) < +infty ;

      then ( Integral (M, |.f.|)) < +infty by A1, A2, A5, A7, MESFUN12: 84;

      then ( integral+ (M, |.f.|)) < +infty by A3, A5, MESFUNC2: 27, MESFUNC5: 88;

      then

       A8: ( integral+ (M,( max+ |.f.|))) < +infty by MESFUN11: 31;

      now

        let z be Element of [:X1, X2:];

        assume z in ( dom ( max- |.f.|));

        (( max+ |.f.|) . z) = ( |.f.| . z) by MESFUN11: 31;

        hence (( max- |.f.|) . z) = 0 by MESFUNC2: 19;

      end;

      then ( integral+ (M,( max- |.f.|))) = 0 by A5, A6, A7, MESFUNC2: 26, MESFUNC5: 87;

      then |.f.| is_integrable_on M by A3, A5, A8, MESFUNC2: 27, MESFUNC5:def 17;

      hence f is_integrable_on M by A3, MESFUNC5: 100;

    end;

    theorem :: MESFUN13:10

    for E be Element of ( sigma ( measurable_rectangles (S1,S2))), f be E -measurable PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & E = ( dom f) holds f is_integrable_on ( Prod_Measure (M1,M2)) iff ( Integral (M2,( Integral1 (M1, |.f.|)))) < +infty by Lm1, Lm2;

    theorem :: MESFUN13:11

    for E be Element of ( sigma ( measurable_rectangles (S1,S2))), f be E -measurable PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & E = ( dom f) holds f is_integrable_on ( Prod_Measure (M1,M2)) iff ( Integral (M1,( Integral2 (M2, |.f.|)))) < +infty by Lm1, Lm2;

    theorem :: MESFUN13:12

    

     Th4: for E be Element of ( sigma ( measurable_rectangles (S1,S2))), U be Element of S1, f be E -measurable PartFunc of [:X1, X2:], ExtREAL st M2 is sigma_finite & E = ( dom f) holds ( Integral2 (M2, |.f.|)) is U -measurable

    proof

      let E be Element of ( sigma ( measurable_rectangles (S1,S2))), U be Element of S1, f be E -measurable PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M2 is sigma_finite and

       A2: E = ( dom f);

      

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

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

      hence ( Integral2 (M2, |.f.|)) is U -measurable by A1, A3, MESFUN12: 60;

    end;

    theorem :: MESFUN13:13

    

     Th5: for E be Element of ( sigma ( measurable_rectangles (S1,S2))), V be Element of S2, f be E -measurable PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & E = ( dom f) holds ( Integral1 (M1, |.f.|)) is V -measurable

    proof

      let E be Element of ( sigma ( measurable_rectangles (S1,S2))), V be Element of S2, f be E -measurable PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: E = ( dom f);

      

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

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

      hence ( Integral1 (M1, |.f.|)) is V -measurable by A1, A3, MESFUN12: 59;

    end;

    theorem :: MESFUN13:14

    for f be PartFunc of [:X1, X2:], ExtREAL st M2 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) holds ( Integral (M1,( max+ ( Integral2 (M2, |.f.|))))) = ( Integral (M1,( Integral2 (M2, |.f.|)))) & ( Integral (M1,( max- ( Integral2 (M2, |.f.|))))) = 0

    proof

      let f be PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M2 is sigma_finite and

       A2: f is_integrable_on ( Prod_Measure (M1,M2));

      consider A be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A3: A = ( dom f) & f is A -measurable by A2, MESFUNC5:def 17;

      reconsider SX1 = X1 as Element of S1 by MEASURE1: 7;

      

       A4: ( Integral2 (M2, |.f.|)) is SX1 -measurable by A1, A3, Th4;

      A = ( dom |.f.|) & |.f.| is A -measurable by A3, MESFUNC1:def 10, MESFUNC2: 27;

      then

       A5: ( Integral2 (M2, |.f.|)) is nonnegative by MESFUN12: 66;

      hence ( Integral (M1,( max+ ( Integral2 (M2, |.f.|))))) = ( Integral (M1,( Integral2 (M2, |.f.|)))) by MESFUN11: 31;

      SX1 = ( dom ( Integral2 (M2, |.f.|))) by FUNCT_2:def 1;

      hence ( Integral (M1,( max- ( Integral2 (M2, |.f.|))))) = 0 by A4, A5, MESFUN11: 53;

    end;

    theorem :: MESFUN13:15

    for f be PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) holds ( Integral (M2,( max+ ( Integral1 (M1, |.f.|))))) = ( Integral (M2,( Integral1 (M1, |.f.|)))) & ( Integral (M2,( max- ( Integral1 (M1, |.f.|))))) = 0

    proof

      let f be PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: f is_integrable_on ( Prod_Measure (M1,M2));

      consider E be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A3: E = ( dom f) & f is E -measurable by A2, MESFUNC5:def 17;

      reconsider SX2 = X2 as Element of S2 by MEASURE1: 7;

      

       A4: ( Integral1 (M1, |.f.|)) is SX2 -measurable by A1, A3, Th5;

      E = ( dom |.f.|) & |.f.| is E -measurable by A3, MESFUNC1:def 10, MESFUNC2: 27;

      then

       A5: ( Integral1 (M1, |.f.|)) is nonnegative by MESFUN12: 66;

      hence ( Integral (M2,( max+ ( Integral1 (M1, |.f.|))))) = ( Integral (M2,( Integral1 (M1, |.f.|)))) by MESFUN11: 31;

      SX2 = ( dom ( Integral1 (M1, |.f.|))) by FUNCT_2:def 1;

      hence ( Integral (M2,( max- ( Integral1 (M1, |.f.|))))) = 0 by A4, A5, MESFUN11: 53;

    end;

    ::$Notion-Name

    theorem :: MESFUN13:16

    

     Th14: for E be Element of S, f be E -measurable PartFunc of X, ExtREAL , er be ExtReal st ( dom f) = E & f is nonnegative & er >= 0 holds (er * (M . ( great_eq_dom (f,er)))) <= ( Integral (M,f))

    proof

      let E be Element of S, f be E -measurable PartFunc of X, ExtREAL , er be ExtReal;

      assume that

       A1: ( dom f) = E and

       A2: f is nonnegative and

       A3: er >= 0 ;

      

       A4: ( great_eq_dom (f,er)) c= E by A1, MESFUNC1:def 14;

      

       A5: ( great_eq_dom (f, +infty )) = ( eq_dom (f, +infty )) by Th10;

      er in REAL or er = +infty by A3, XXREAL_0: 14;

      then (E /\ ( great_eq_dom (f,er))) is Element of S by A1, A5, MESFUNC1: 27, MESFUNC1: 33;

      then

      reconsider Er = ( great_eq_dom (f,er)) as Element of S by A4, XBOOLE_1: 28;

      ( dom ( chi (er,Er,X))) = X by FUNCT_2:def 1;

      then

       A6: Er = ( dom (f | Er)) & Er = ( dom (( chi (er,Er,X)) | Er)) by A1, A4, RELAT_1: 62;

      f is Er -measurable & Er = (Er /\ ( dom f)) by A1, A4, XBOOLE_1: 28, MESFUNC1: 30;

      then

       A7: (f | Er) is Er -measurable by MESFUNC5: 42;

      

       A8: (f | Er) is nonnegative by A2, MESFUNC5: 15;

      

       A9: (( chi (er,Er,X)) | Er) is Er -measurable by MESFUN12: 15;

      ( chi (er,Er,X)) is nonnegative by A3, MESFUN12: 17;

      then

       A10: (( chi (er,Er,X)) | Er) is nonnegative by MESFUNC5: 15;

      for x be Element of X st x in ( dom (( chi (er,Er,X)) | Er)) holds ((( chi (er,Er,X)) | Er) . x) <= ((f | Er) . x)

      proof

        let x be Element of X;

        assume

         A11: x in ( dom (( chi (er,Er,X)) | Er));

        then ((( chi (er,Er,X)) | Er) . x) = (( chi (er,Er,X)) . x) by FUNCT_1: 47;

        then

         A12: ((( chi (er,Er,X)) | Er) . x) = er by A6, A11, MESFUN12:def 1;

        

         A13: ((f | Er) . x) = (f . x) by A6, A11, FUNCT_1: 47;

        x in ( great_eq_dom (f,er)) by A11, RELAT_1: 57;

        hence ((( chi (er,Er,X)) | Er) . x) <= ((f | Er) . x) by A12, A13, MESFUNC1:def 14;

      end;

      then ( integral+ (M,(( chi (er,Er,X)) | Er))) <= ( integral+ (M,(f | Er))) by A6, A7, A8, A9, A10, MESFUNC5: 85;

      then ( Integral (M,(( chi (er,Er,X)) | Er))) <= ( integral+ (M,(f | Er))) by A6, A10, MESFUNC5: 88, MESFUN12: 15;

      then

       A14: (er * (M . Er)) <= ( integral+ (M,(f | Er))) by MESFUN12: 50;

      ( integral+ (M,(f | Er))) <= ( integral+ (M,(f | E))) by A1, A2, A4, MESFUNC5: 83;

      then ( integral+ (M,(f | Er))) <= ( Integral (M,f)) by A1, A2, MESFUNC5: 88;

      hence (er * (M . ( great_eq_dom (f,er)))) <= ( Integral (M,f)) by A14, XXREAL_0: 2;

    end;

    begin

    theorem :: MESFUN13:17

    

     Th21: for f,g be PartFunc of X, ExtREAL st f is_integrable_on M & g is_integrable_on M holds ( Integral (M,(f + g))) = (( Integral (M,(f | (( dom f) /\ ( dom g))))) + ( Integral (M,(g | (( dom f) /\ ( dom g)))))) & ( Integral (M,(f - g))) = (( Integral (M,(f | (( dom f) /\ ( dom g))))) - ( Integral (M,(g | (( dom f) /\ ( dom g))))))

    proof

      let f,g be PartFunc of X, ExtREAL ;

      assume that

       A1: f is_integrable_on M and

       A2: g is_integrable_on M;

      consider E be Element of S such that

       A3: E = (( dom f) /\ ( dom g)) & ( Integral (M,(f + g))) = (( Integral (M,(f | E))) + ( Integral (M,(g | E)))) by A1, A2, MESFUNC5: 109;

      thus ( Integral (M,(f + g))) = (( Integral (M,(f | (( dom f) /\ ( dom g))))) + ( Integral (M,(g | (( dom f) /\ ( dom g)))))) by A3;

      ex E0 be Element of S st E0 = ( dom g) & g is E0 -measurable by A2, MESFUNC5:def 17;

      then

       A4: g is E -measurable by A3, XBOOLE_1: 17, MESFUNC1: 30;

      ex E be Element of S st E = (( dom f) /\ ( dom g)) & ( Integral (M,(f - g))) = (( Integral (M,(f | E))) + ( Integral (M,(( - g) | E)))) by A1, A2, MESFUN10: 13;

      then ( Integral (M,(f - g))) = (( Integral (M,(f | E))) + ( - ( Integral (M,(g | E))))) by A3, A4, XBOOLE_1: 17, MESFUN11: 55;

      hence ( Integral (M,(f - g))) = (( Integral (M,(f | (( dom f) /\ ( dom g))))) - ( Integral (M,(g | (( dom f) /\ ( dom g)))))) by A3, XXREAL_3:def 4;

    end;

    theorem :: MESFUN13:18

    for f be PartFunc of X, ExtREAL holds f is_integrable_on M iff ( max+ f) is_integrable_on M & ( max- f) is_integrable_on M

    proof

      let f be PartFunc of X, ExtREAL ;

      hereby

        assume

         A1: f is_integrable_on M;

        then

        consider E be Element of S such that

         A2: E = ( dom f) & f is E -measurable by MESFUNC5:def 17;

        

         A3: ( integral+ (M,( max+ f))) < +infty & ( integral+ (M,( max- f))) < +infty by A1, MESFUNC5:def 17;

        

         A4: E = ( dom ( max+ f)) & E = ( dom ( max- f)) by A2, MESFUNC2:def 2, MESFUNC2:def 3;

        

         A5: ( max+ f) is E -measurable & ( max- f) is E -measurable by A2, MESFUN11: 10;

        

         A6: ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

        then

         A7: ( integral+ (M,( max+ ( max+ f)))) < +infty & ( integral+ (M,( max+ ( max- f)))) < +infty by A3, MESFUN11: 31;

        ( integral+ (M,( max- ( max+ f)))) < +infty & ( integral+ (M,( max- ( max- f)))) < +infty by A4, A5, A6, MESFUN11: 53;

        hence ( max+ f) is_integrable_on M & ( max- f) is_integrable_on M by A4, A5, A7, MESFUNC5:def 17;

      end;

      assume that

       A8: ( max+ f) is_integrable_on M and

       A9: ( max- f) is_integrable_on M;

      consider E1 be Element of S such that

       A10: E1 = ( dom ( max+ f)) & ( max+ f) is E1 -measurable by A8, MESFUNC5:def 17;

      consider E2 be Element of S such that

       A11: E2 = ( dom ( max- f)) & ( max- f) is E2 -measurable by A9, MESFUNC5:def 17;

      

       A12: E1 = ( dom f) by A10, MESFUNC2:def 2;

      then E1 = E2 by A11, MESFUNC2:def 3;

      then

       A13: f is E1 -measurable by A10, A11, A12, MESFUN11: 10;

      ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

      then ( max+ ( max+ f)) = ( max+ f) & ( max+ ( max- f)) = ( max- f) by MESFUN11: 31;

      then ( integral+ (M,( max+ f))) < +infty & ( integral+ (M,( max- f))) < +infty by A8, A9, MESFUNC5:def 17;

      hence f is_integrable_on M by A12, A13, MESFUNC5:def 17;

    end;

    theorem :: MESFUN13:19

    for A,B be Element of S, f be PartFunc of X, ExtREAL st B c= A & (f | A) is B -measurable holds f is B -measurable

    proof

      let A,B be Element of S, f be PartFunc of X, ExtREAL ;

      assume that

       A1: B c= A and

       A2: (f | A) is B -measurable;

      let r be Real;

      now

        let x be object;

        assume x in (B /\ ( less_dom ((f | A),r)));

        then

         A3: x in B & x in ( less_dom ((f | A),r)) by XBOOLE_0:def 4;

        then x in ( dom (f | A)) & ((f | A) . x) < r by MESFUNC1:def 11;

        then x in ( dom f) & (f . x) < r by RELAT_1: 57, FUNCT_1: 47;

        then x in ( less_dom (f,r)) by MESFUNC1:def 11;

        hence x in (B /\ ( less_dom (f,r))) by A3, XBOOLE_0:def 4;

      end;

      then

       A4: (B /\ ( less_dom ((f | A),r))) c= (B /\ ( less_dom (f,r)));

      now

        let x be object;

        assume x in (B /\ ( less_dom (f,r)));

        then

         A5: x in B & x in ( less_dom (f,r)) by XBOOLE_0:def 4;

        then x in ( dom f) & (f . x) < r by MESFUNC1:def 11;

        then x in ( dom (f | A)) & ((f | A) . x) < r by A1, A5, RELAT_1: 57, FUNCT_1: 49;

        then x in ( less_dom ((f | A),r)) by MESFUNC1:def 11;

        hence x in (B /\ ( less_dom ((f | A),r))) by A5, XBOOLE_0:def 4;

      end;

      then (B /\ ( less_dom (f,r))) c= (B /\ ( less_dom ((f | A),r)));

      then (B /\ ( less_dom ((f | A),r))) = (B /\ ( less_dom (f,r))) by A4;

      hence (B /\ ( less_dom (f,r))) in S by A2;

    end;

    definition

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL ;

      :: MESFUN13:def1

      pred f is_a.e.integrable_on M means ex A be Element of S st (M . A) = 0 & A c= ( dom f) & (f | (A ` )) is_integrable_on M;

    end

    theorem :: MESFUN13:20

    

     Th16: for f be PartFunc of X, ExtREAL st f is_a.e.integrable_on M holds ( dom f) in S

    proof

      let f be PartFunc of X, ExtREAL ;

      assume f is_a.e.integrable_on M;

      then

      consider A be Element of S such that

       A1: (M . A) = 0 & A c= ( dom f) & (f | (A ` )) is_integrable_on M;

      consider B be Element of S such that

       A2: B = ( dom (f | (A ` ))) & (f | (A ` )) is B -measurable by A1, MESFUNC5:def 17;

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

      .= (( dom f) /\ (X \ A)) by SUBSET_1:def 4

      .= ((( dom f) /\ X) \ A) by XBOOLE_1: 49

      .= (( dom f) \ A) by XBOOLE_1: 28;

      then ( dom f) = (A \/ B) by A1, A2, XBOOLE_1: 45;

      hence ( dom f) in S;

    end;

    theorem :: MESFUN13:21

    for f be PartFunc of X, ExtREAL st f is_integrable_on M holds f is_a.e.integrable_on M

    proof

      let f be PartFunc of X, ExtREAL ;

      assume

       A1: f is_integrable_on M;

      reconsider A = {} , XX = X as Element of S by MEASURE1: 7;

      

       A2: (M . A) = 0 & A c= ( dom f) & (f | (( dom f) \ A)) is_integrable_on M by A1, VALUED_0:def 19;

      then (f | (A ` )) is_integrable_on M by Th15;

      hence thesis by A2;

    end;

    definition

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL ;

      :: MESFUN13:def2

      pred f is_a.e.finite M means ex A be Element of S st (M . A) = 0 & A c= ( dom f) & (f | (A ` )) is PartFunc of X, REAL ;

    end

    theorem :: MESFUN13:22

    for E be Element of S, f be E -measurable PartFunc of X, ExtREAL st ( dom f) = E holds f is_a.e.finite M iff (M . (( eq_dom (f, +infty )) \/ ( eq_dom (f, -infty )))) = 0

    proof

      let E be Element of S, f be E -measurable PartFunc of X, ExtREAL ;

      assume ( dom f) = E;

      then

      reconsider E01 = ( eq_dom (f, +infty )), E02 = ( eq_dom (f, -infty )) as Element of S by Th9;

      

       A1: E01 c= ( dom f) & E02 c= ( dom f) by MESFUNC1:def 15;

      hereby

        assume f is_a.e.finite M;

        then

        consider A be Element of S such that

         A2: (M . A) = 0 & A c= ( dom f) & (f | (A ` )) is PartFunc of X, REAL ;

        now

          assume ex x be object st x in (E01 \/ E02) & not x in A;

          then

          consider x be object such that

           A3: x in (E01 \/ E02) & not x in A;

          x in E01 or x in E02 by A3, XBOOLE_0:def 3;

          then

           A4: x in ( dom f) & ((f . x) = +infty or (f . x) = -infty ) by MESFUNC1:def 15;

          x in (X \ A) by A3, XBOOLE_0:def 5;

          then

           A5: x in (A ` ) by SUBSET_1:def 4;

          then x in ( dom (f | (A ` ))) by A4, RELAT_1: 57;

          then ((f | (A ` )) . x) in REAL by A2, PARTFUN1: 4;

          hence contradiction by A4, A5, FUNCT_1: 49;

        end;

        then (E01 \/ E02) c= A;

        then (M . (E01 \/ E02)) <= 0 by A2, MEASURE1: 8;

        hence (M . (( eq_dom (f, +infty )) \/ ( eq_dom (f, -infty )))) = 0 by MEASURE1:def 2;

      end;

      assume

       A6: (M . (( eq_dom (f, +infty )) \/ ( eq_dom (f, -infty )))) = 0 ;

      now

        let y be object;

        assume y in ( rng (f | ((E01 \/ E02) ` )));

        then

        consider x be object such that

         A7: x in ( dom (f | ((E01 \/ E02) ` ))) & ((f | ((E01 \/ E02) ` )) . x) = y by FUNCT_1:def 3;

        ( dom (f | ((E01 \/ E02) ` ))) c= ((E01 \/ E02) ` ) by RELAT_1: 58;

        then x in ((E01 \/ E02) ` ) by A7;

        then x in (X \ (E01 \/ E02)) by SUBSET_1:def 4;

        then not x in (E01 \/ E02) by XBOOLE_0:def 5;

        then

         A8: not x in E01 & not x in E02 by XBOOLE_0:def 3;

        ( dom (f | ((E01 \/ E02) ` ))) c= ( dom f) by RELAT_1: 60;

        then (f . x) <> +infty & (f . x) <> -infty by A7, A8, MESFUNC1:def 15;

        then (f . x) in REAL by XXREAL_0: 14;

        hence y in REAL by A7, FUNCT_1: 47;

      end;

      then ( rng (f | ((E01 \/ E02) ` ))) c= REAL ;

      then (f | ((E01 \/ E02) ` )) is PartFunc of X, REAL by RELSET_1: 6;

      hence f is_a.e.finite M by A1, A6, XBOOLE_1: 8;

    end;

    theorem :: MESFUN13:23

    

     Th19: for f be PartFunc of X, ExtREAL st f is_integrable_on M holds (M . ( eq_dom (f, +infty ))) = 0 & (M . ( eq_dom (f, -infty ))) = 0 & f is_a.e.finite M & for r be Real st r > 0 holds (M . ( great_eq_dom ( |.f.|,r))) < +infty

    proof

      let f be PartFunc of X, ExtREAL ;

      assume

       A2: f is_integrable_on M;

      consider E be Element of S such that

       A3: E = ( dom f) & f is E -measurable by A2, MESFUNC5:def 17;

      ( eq_dom (f, +infty )) c= E by A3, MESFUNC1:def 15;

      then ( eq_dom (f, +infty )) = (E /\ ( eq_dom (f, +infty ))) by XBOOLE_1: 28;

      then

      reconsider E0 = ( eq_dom (f, +infty )) as Element of S by A3, MESFUNC1: 33;

      ( eq_dom (f, -infty )) c= E by A3, MESFUNC1:def 15;

      then ( eq_dom (f, -infty )) = (E /\ ( eq_dom (f, -infty ))) by XBOOLE_1: 28;

      then

      reconsider E1 = ( eq_dom (f, -infty )) as Element of S by A3, MESFUNC1: 34;

      

       A4: E0 c= E & E1 c= E by A3, MESFUNC1:def 15;

      then

       A5: E0 = (E /\ E0) & E1 = (E /\ E1) & (E0 \/ E1) c= E by XBOOLE_1: 8, XBOOLE_1: 28;

      

       A6: ( dom ( max+ f)) = E & ( dom ( max- f)) = E & ( dom |.f.|) = E by A3, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;

      then

       A7: ( dom (f | E0)) = E0 & ( dom (( max+ f) | E0)) = E0 & ( dom (f | E1)) = E1 & ( dom (( max- f) | E1)) = E1 by A3, A4, RELAT_1: 62;

      

       A8: ( max+ f) is E -measurable & ( max- f) is E -measurable & |.f.| is E -measurable by A3, MESFUNC2: 25, MESFUNC2: 26, MESFUNC2: 27;

      then

       A9: ( max+ f) is E0 -measurable & ( max- f) is E1 -measurable by A4, MESFUNC1: 30;

      

       A10: (( max+ f) | E0) is nonnegative & (( max- f) | E1) is nonnegative by MESFUNC5: 15, MESFUN11: 5;

      

       A11: ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

      then ( integral+ (M,(( max+ f) | E0))) <= ( integral+ (M,(( max+ f) | E))) by A3, A4, A6, MESFUNC2: 25, MESFUNC5: 83;

      then ( integral+ (M,(( max+ f) | E0))) < +infty by A2, A6, MESFUNC5:def 17, XXREAL_0: 2;

      then

       A12: ( Integral (M,(( max+ f) | E0))) < +infty by A5, A6, A7, A9, A10, MESFUNC5: 42, MESFUNC5: 88;

       A13:

      now

        let x be Element of X;

        assume

         A14: x in ( dom (f | E0));

        then x in E0 by RELAT_1: 57;

        then x in ( dom f) & (f . x) = +infty by MESFUNC1:def 15;

        hence ((f | E0) . x) = +infty by A14, FUNCT_1: 47;

      end;

      now

        let x be Element of X;

        assume

         A15: x in ( dom (f | E0));

        then

         A16: ((f | E0) . x) = +infty by A13;

        then

         A17: x in ( dom f) & (f . x) = +infty by A15, RELAT_1: 57, FUNCT_1: 47;

        then x in ( dom ( max+ f)) by MESFUNC2:def 2;

        then (( max+ f) . x) = ( max ( +infty , 0 )) by A17, MESFUNC2:def 2;

        then (( max+ f) . x) = +infty by XXREAL_0:def 10;

        hence ((f | E0) . x) = ((( max+ f) | E0) . x) by A7, A15, A16, FUNCT_1: 47;

      end;

      then

       A18: ( Integral (M,(f | E0))) < +infty by A7, A12, PARTFUN1: 5;

      ( dom ( chi ( +infty ,E0,X))) = X by FUNCT_2:def 1;

      then

       A19: ( dom (( chi ( +infty ,E0,X)) | E0)) = E0 by RELAT_1: 62;

      now

        let x be Element of X;

        assume

         A20: x in ( dom (f | E0));

        then

         A21: x in E0 by RELAT_1: 57;

        then ((( chi ( +infty ,E0,X)) | E0) . x) = (( chi ( +infty ,E0,X)) . x) by FUNCT_1: 49;

        then ((( chi ( +infty ,E0,X)) | E0) . x) = +infty by A21, MESFUN12:def 1;

        hence ((f | E0) . x) = ((( chi ( +infty ,E0,X)) | E0) . x) by A13, A20;

      end;

      then (f | E0) = (( chi ( +infty ,E0,X)) | E0) by A3, A4, A19, RELAT_1: 62, PARTFUN1: 5;

      then

       A22: ( Integral (M,(f | E0))) = ( +infty * (M . E0)) by MESFUN12: 50;

       A23:

      now

        assume (M . E0) <> 0 ;

        then (M . E0) > 0 by SUPINF_2: 51;

        hence contradiction by A18, A22, XXREAL_3:def 5;

      end;

      hence (M . ( eq_dom (f, +infty ))) = 0 ;

      

       A24: ( Integral (M,( - (( max- f) | E1)))) = ( - ( Integral (M,(( max- f) | E1)))) by A5, A6, A7, A9, MESFUNC5: 42, MESFUN11: 52;

      ( integral+ (M,(( max- f) | E1))) <= ( integral+ (M,(( max- f) | E))) by A3, A4, A6, A11, MESFUNC2: 26, MESFUNC5: 83;

      then ( integral+ (M,(( max- f) | E1))) < +infty by A2, A6, MESFUNC5:def 17, XXREAL_0: 2;

      then ( Integral (M,(( max- f) | E1))) < +infty by A5, A6, A7, A9, A10, MESFUNC5: 42, MESFUNC5: 88;

      then

       A25: ( Integral (M,( - (( max- f) | E1)))) > -infty by A24, XXREAL_3: 6, XXREAL_3: 38;

       A26:

      now

        let x be Element of X;

        assume

         d7: x in ( dom (f | E1));

        then x in E1 by RELAT_1: 57;

        then x in ( dom f) & (f . x) = -infty by MESFUNC1:def 15;

        hence ((f | E1) . x) = -infty by d7, FUNCT_1: 47;

      end;

      

       A27: ( dom ( - (( max- f) | E1))) = E1 by A7, MESFUNC1:def 7;

      now

        let x be Element of X;

        assume

         A28: x in ( dom (f | E1));

        then x in E1 by RELAT_1: 57;

        then

         A29: x in ( dom f) & (f . x) = -infty by MESFUNC1:def 15;

        then

         A30: ((f | E1) . x) = ( - +infty ) by A28, FUNCT_1: 47, XXREAL_3: 6;

        x in ( dom ( max- f)) by A29, MESFUNC2:def 3;

        then (( max- f) . x) = ( max (( - -infty ), 0 )) by A29, MESFUNC2:def 3;

        then (( max- f) . x) = +infty by XXREAL_0:def 10, XXREAL_3: 5;

        then ((f | E1) . x) = ( - ((( max- f) | E1) . x)) by A7, A28, A30, FUNCT_1: 47;

        hence ((f | E1) . x) = (( - (( max- f) | E1)) . x) by A7, A27, A28, MESFUNC1:def 7;

      end;

      then

       A31: ( Integral (M,(f | E1))) > -infty by A3, A4, A25, A27, RELAT_1: 62, PARTFUN1: 5;

      ( dom ( chi ( -infty ,E1,X))) = X by FUNCT_2:def 1;

      then

       A32: ( dom (( chi ( -infty ,E1,X)) | E1)) = E1 by RELAT_1: 62;

      now

        let x be Element of X;

        assume

         A33: x in ( dom (f | E1));

        then

         A34: x in E1 by RELAT_1: 57;

        then ((( chi ( -infty ,E1,X)) | E1) . x) = (( chi ( -infty ,E1,X)) . x) by FUNCT_1: 49;

        then ((( chi ( -infty ,E1,X)) | E1) . x) = -infty by A34, MESFUN12:def 1;

        hence ((f | E1) . x) = ((( chi ( -infty ,E1,X)) | E1) . x) by A26, A33;

      end;

      then (f | E1) = (( chi ( -infty ,E1,X)) | E1) by A3, A4, A32, RELAT_1: 62, PARTFUN1: 5;

      then

       A35: ( Integral (M,(f | E1))) = ( -infty * (M . E1)) by MESFUN12: 50;

       A36:

      now

        assume (M . E1) <> 0 ;

        then (M . E1) > 0 by SUPINF_2: 51;

        hence contradiction by A31, A35, XXREAL_3:def 5;

      end;

      hence (M . ( eq_dom (f, -infty ))) = 0 ;

      set E2 = (E0 \/ E1);

      (M . E2) <= ((M . E0) + (M . E1)) by MEASURE1: 33;

      then (M . E2) <= 0 & (M . E2) >= 0 by A23, A36, SUPINF_2: 51;

      then

       A37: (M . E2) = 0 ;

      now

        let r be ExtReal;

        assume r in ( rng (f | (E2 ` )));

        then

        consider x be object such that

         A38: x in ( dom (f | (E2 ` ))) & r = ((f | (E2 ` )) . x) by FUNCT_1:def 3;

        

         A39: x in ( dom f) & x in (E2 ` ) by A38, RELAT_1: 57;

        then x in (X \ E2) by SUBSET_1:def 4;

        then x in X & not x in E2 by XBOOLE_0:def 5;

        then not x in E0 & not x in E1 by XBOOLE_0:def 3;

        then (f . x) <> +infty & (f . x) <> -infty by A39, MESFUNC1:def 15;

        then r <> +infty & r <> -infty by A38, FUNCT_1: 47;

        hence r in REAL by XXREAL_0: 14;

      end;

      then ( rng (f | (E2 ` ))) c= REAL ;

      then (f | (E2 ` )) is PartFunc of X, REAL by RELSET_1: 6;

      hence f is_a.e.finite M by A3, A4, A37, XBOOLE_1: 8;

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

      then

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

      thus for r be Real st r > 0 holds (M . ( great_eq_dom ( |.f.|,r))) < +infty

      proof

        let r be Real;

        assume

         A41: r > 0 ;

        then (r * (M . ( great_eq_dom ( |.f.|,r)))) <= ( Integral (M, |.f.|)) by A6, A8, Th14;

        then (r * (M . ( great_eq_dom ( |.f.|,r)))) < +infty by A40, XXREAL_0: 2;

        then ((r * (M . ( great_eq_dom ( |.f.|,r)))) / r) < ( +infty / r) by A41, XXREAL_3: 80;

        then (M . ( great_eq_dom ( |.f.|,r))) < ( +infty / r) by A41, XXREAL_3: 88;

        hence (M . ( great_eq_dom ( |.f.|,r))) < +infty by A41, XXREAL_3: 83;

      end;

    end;

    theorem :: MESFUN13:24

    

     Th20: for f be PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) holds ( Integral1 (M1,( max+ f))) is_integrable_on M2 & ( Integral2 (M2,( max+ f))) is_integrable_on M1 & ( Integral1 (M1,( max- f))) is_integrable_on M2 & ( Integral2 (M2,( max- f))) is_integrable_on M1 & ( Integral1 (M1, |.f.|)) is_integrable_on M2 & ( Integral2 (M2, |.f.|)) is_integrable_on M1

    proof

      let f be PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: f is_integrable_on ( Prod_Measure (M1,M2));

      reconsider XX1 = X1 as Element of S1 by MEASURE1: 7;

      reconsider XX2 = X2 as Element of S2 by MEASURE1: 7;

      set PM = ( Prod_Measure (M1,M2));

      consider E be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A4: E = ( dom f) & f is E -measurable by A3, MESFUNC5:def 17;

      

       A5: ( max+ f) is E -measurable & ( max- f) is E -measurable & |.f.| is E -measurable by A4, MESFUNC2: 27, MESFUN11: 10;

      

       A6: ( dom ( max+ f)) = E & ( dom ( max- f)) = E & ( dom |.f.|) = E by A4, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;

      

       A7: ( max+ f) is nonnegative & ( max- f) is nonnegative & |.f.| is nonnegative by MESFUN11: 5;

      then

       A8: ( Integral1 (M1,( max+ f))) is nonnegative & ( Integral2 (M2,( max+ f))) is nonnegative & ( Integral1 (M1,( max- f))) is nonnegative & ( Integral2 (M2,( max- f))) is nonnegative & ( Integral1 (M1, |.f.|)) is nonnegative & ( Integral2 (M2, |.f.|)) is nonnegative by A5, A6, MESFUN12: 66;

      

       A9: ( Integral1 (M1,( max+ f))) is XX2 -measurable & ( Integral1 (M1,( max- f))) is XX2 -measurable & ( Integral1 (M1, |.f.|)) is XX2 -measurable & ( Integral2 (M2,( max+ f))) is XX1 -measurable & ( Integral2 (M2,( max- f))) is XX1 -measurable & ( Integral2 (M2, |.f.|)) is XX1 -measurable by A1, A2, A5, A6, MESFUN11: 5, MESFUN12: 59, MESFUN12: 60;

      

       A10: ( dom ( Integral1 (M1,( max+ f)))) = XX2 & ( dom ( Integral2 (M2,( max+ f)))) = XX1 & ( dom ( Integral1 (M1,( max- f)))) = XX2 & ( dom ( Integral2 (M2,( max- f)))) = XX1 & ( dom ( Integral1 (M1, |.f.|))) = XX2 & ( dom ( Integral2 (M2, |.f.|))) = XX1 by FUNCT_2:def 1;

      ( integral+ (PM,( max+ f))) = ( Integral (PM,( max+ f))) & ( integral+ (PM,( max- f))) = ( Integral (PM,( max- f))) by A5, A6, MESFUN11: 5, MESFUNC5: 88;

      then ( integral+ (PM,( max+ f))) = ( Integral (M2,( Integral1 (M1,( max+ f))))) & ( integral+ (PM,( max+ f))) = ( Integral (M1,( Integral2 (M2,( max+ f))))) & ( integral+ (PM,( max- f))) = ( Integral (M2,( Integral1 (M1,( max- f))))) & ( integral+ (PM,( max- f))) = ( Integral (M1,( Integral2 (M2,( max- f))))) by A1, A2, A5, A6, A7, MESFUN12: 84;

      then

       A11: ( Integral (M2,( Integral1 (M1,( max+ f))))) < +infty & ( Integral (M1,( Integral2 (M2,( max+ f))))) < +infty & ( Integral (M2,( Integral1 (M1,( max- f))))) < +infty & ( Integral (M1,( Integral2 (M2,( max- f))))) < +infty by A3, MESFUNC5:def 17;

      ( Integral1 (M1,( max+ f))) = ( max+ ( Integral1 (M1,( max+ f)))) & ( Integral2 (M2,( max+ f))) = ( max+ ( Integral2 (M2,( max+ f)))) & ( Integral1 (M1,( max- f))) = ( max+ ( Integral1 (M1,( max- f)))) & ( Integral2 (M2,( max- f))) = ( max+ ( Integral2 (M2,( max- f)))) by A8, MESFUN11: 31;

      then

       A12: ( integral+ (M2,( max+ ( Integral1 (M1,( max+ f)))))) < +infty & ( integral+ (M1,( max+ ( Integral2 (M2,( max+ f)))))) < +infty & ( integral+ (M2,( max+ ( Integral1 (M1,( max- f)))))) < +infty & ( integral+ (M1,( max+ ( Integral2 (M2,( max- f)))))) < +infty by A8, A9, A10, A11, MESFUNC5: 88;

      ( integral+ (M2,( max- ( Integral1 (M1,( max+ f)))))) = 0 & ( integral+ (M1,( max- ( Integral2 (M2,( max+ f)))))) = 0 & ( integral+ (M2,( max- ( Integral1 (M1,( max- f)))))) = 0 & ( integral+ (M1,( max- ( Integral2 (M2,( max- f)))))) = 0 by A8, A9, A10, MESFUN11: 53;

      hence ( Integral1 (M1,( max+ f))) is_integrable_on M2 & ( Integral2 (M2,( max+ f))) is_integrable_on M1 & ( Integral1 (M1,( max- f))) is_integrable_on M2 & ( Integral2 (M2,( max- f))) is_integrable_on M1 by A9, A10, A12, MESFUNC5:def 17;

      

       A13: |.f.| is_integrable_on ( Prod_Measure (M1,M2)) by A3, A4, MESFUNC5: 100;

      ( max+ |.f.|) = |.f.| by MESFUN11: 31;

      then ( integral+ (PM,( max+ |.f.|))) = ( Integral (PM, |.f.|)) by A6, A4, MESFUNC2: 27, MESFUNC5: 88;

      then ( integral+ (PM,( max+ |.f.|))) = ( Integral (M2,( Integral1 (M1, |.f.|)))) & ( integral+ (PM,( max+ |.f.|))) = ( Integral (M1,( Integral2 (M2, |.f.|)))) by A1, A2, A5, A6, MESFUN12: 84;

      then

       A15: ( Integral (M2,( Integral1 (M1, |.f.|)))) < +infty & ( Integral (M1,( Integral2 (M2, |.f.|)))) < +infty by A13, MESFUNC5:def 17;

      ( Integral1 (M1, |.f.|)) = ( max+ ( Integral1 (M1, |.f.|))) & ( Integral2 (M2, |.f.|)) = ( max+ ( Integral2 (M2, |.f.|))) by A8, MESFUN11: 31;

      then

       A16: ( integral+ (M2,( max+ ( Integral1 (M1, |.f.|))))) < +infty & ( integral+ (M1,( max+ ( Integral2 (M2, |.f.|))))) < +infty by A8, A9, A10, A15, MESFUNC5: 88;

      ( integral+ (M2,( max- ( Integral1 (M1, |.f.|))))) = 0 & ( integral+ (M1,( max- ( Integral2 (M2, |.f.|))))) = 0 by A8, A9, A10, MESFUN11: 53;

      hence ( Integral1 (M1, |.f.|)) is_integrable_on M2 & ( Integral2 (M2, |.f.|)) is_integrable_on M1 by A9, A10, A16, MESFUNC5:def 17;

    end;

    theorem :: MESFUN13:25

    for E be Element of S, f be E -measurable PartFunc of X, ExtREAL st ( dom f) c= E & f is_a.e.integrable_on M holds f is_integrable_on M

    proof

      let E be Element of S, f be E -measurable PartFunc of X, ExtREAL ;

      assume that

       A1: ( dom f) c= E and

       A2: f is_a.e.integrable_on M;

      reconsider E1 = ( dom f) as Element of S by A2, Th16;

      consider A be Element of S such that

       A3: (M . A) = 0 & A c= ( dom f) & (f | (A ` )) is_integrable_on M by A2;

      

       A4: (f | (A ` )) = (f | (( dom f) \ A)) by Th15;

      then

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

      

      then

       A6: ( dom (f | (A ` ))) = ((E1 /\ E1) \ A) by XBOOLE_1: 49

      .= (E1 \ A);

      then

       A7: ( dom ( max+ (f | (A ` )))) = (E1 \ A) & ( dom ( max- (f | (A ` )))) = (E1 \ A) by MESFUNC2:def 2, MESFUNC2:def 3;

      

       A8: f is E1 -measurable by A1, MESFUNC1: 30;

      then f is (E1 \ A) -measurable by XBOOLE_1: 36, MESFUNC1: 30;

      then (f | (A ` )) is (E1 \ A) -measurable by A4, A5, A6, MESFUNC5: 42;

      then

       A9: ( max+ (f | (A ` ))) is (E1 \ A) -measurable & ( max- (f | (A ` ))) is (E1 \ A) -measurable by A6, MESFUNC2: 25, MESFUNC2: 26;

      

       A10: E1 = ( dom ( max+ f)) & E1 = ( dom ( max- f)) by MESFUNC2:def 2, MESFUNC2:def 3;

      

       A11: ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

      ( Integral (M,(( max+ f) | (( dom f) \ A)))) = ( Integral (M,( max+ f))) & ( Integral (M,(( max- f) | (( dom f) \ A)))) = ( Integral (M,( max- f))) by A3, A8, A10, MESFUNC2: 25, MESFUNC2: 26, MESFUNC5: 95;

      then ( Integral (M,( max+ (f | (A ` ))))) = ( Integral (M,( max+ f))) & ( Integral (M,( max- (f | (A ` ))))) = ( Integral (M,( max- f))) by A4, MESFUNC5: 28;

      then ( integral+ (M,( max+ (f | (A ` ))))) = ( Integral (M,( max+ f))) & ( integral+ (M,( max- (f | (A ` ))))) = ( Integral (M,( max- f))) by A7, A9, MESFUNC5: 88, MESFUN11: 5;

      then

       A12: ( integral+ (M,( max+ (f | (A ` ))))) = ( integral+ (M,( max+ f))) & ( integral+ (M,( max- (f | (A ` ))))) = ( integral+ (M,( max- f))) by A8, A10, A11, MESFUNC2: 25, MESFUNC2: 26, MESFUNC5: 88;

      ( integral+ (M,( max+ (f | (A ` ))))) < +infty & ( integral+ (M,( max- (f | (A ` ))))) < +infty by A3, MESFUNC5:def 17;

      hence f is_integrable_on M by A8, A12, MESFUNC5:def 17;

    end;

    theorem :: MESFUN13:26

    

     Th23: for A be Element of S, f be PartFunc of X, ExtREAL st (M . A) = 0 & A c= ( dom f) & (f | (A ` )) is_integrable_on M holds ex g be PartFunc of X, ExtREAL st ( dom g) = ( dom f) & (f | (A ` )) = (g | (A ` )) & g is_integrable_on M & ( Integral (M,(f | (A ` )))) = ( Integral (M,g))

    proof

      let A be Element of S, f be PartFunc of X, ExtREAL ;

      assume that

       A2: (M . A) = 0 and

       A1: A c= ( dom f) and

       A3: (f | (A ` )) is_integrable_on M;

      consider B be Element of S such that

       A4: B = ( dom (f | (A ` ))) & (f | (A ` )) is B -measurable by A3, MESFUNC5:def 17;

      

       A5: (f | (A ` )) = (f | (( dom f) \ A)) by Th15;

      

      then

       A6: B = (( dom f) /\ (( dom f) \ A)) by A4, RELAT_1: 61

      .= ((( dom f) /\ ( dom f)) \ A) by XBOOLE_1: 49

      .= (( dom f) \ A);

      then

       A7: ( dom f) = (A \/ B) by A1, XBOOLE_1: 45;

      

       A8: (ex E be Element of S st E = ( dom (f | B)) & (f | B) is E -measurable) & ( integral+ (M,( max+ (f | B)))) < +infty & ( integral+ (M,( max- (f | B)))) < +infty by A3, A5, A6, MESFUNC5:def 17;

      defpred C[ object] means $1 in A;

      deffunc F( object) = +infty ;

      deffunc G( object) = (f . $1);

      consider g be Function such that

       A9: ( dom g) = ( dom f) & for x be object st x in ( dom f) holds ( C[x] implies (g . x) = F(x)) & ( not C[x] implies (g . x) = G(x)) from PARTFUN1:sch 1;

      now

        let y be object;

        assume y in ( rng g);

        then

        consider x be object such that

         A10: x in ( dom g) & y = (g . x) by FUNCT_1:def 3;

        per cases ;

          suppose x in A;

          then (g . x) = +infty by A9, A10;

          hence y in ExtREAL by A10, XXREAL_0:def 1;

        end;

          suppose not x in A;

          then (g . x) = (f . x) by A9, A10;

          then (g . x) in ( rng f) by A9, A10, FUNCT_1: 3;

          hence y in ExtREAL by A10;

        end;

      end;

      then ( rng g) c= ExtREAL ;

      then

      reconsider g as PartFunc of X, ExtREAL by A9, RELSET_1: 4;

      take g;

      thus ( dom g) = ( dom f) by A9;

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

      then

       A11: ( dom (f | (A ` ))) = ( dom (g | (A ` ))) by A9, RELAT_1: 61;

      now

        let x be Element of X;

        assume x in ( dom (f | (A ` )));

        then

         A12: x in ( dom f) & x in (A ` ) by RELAT_1: 57;

        then x in (X \ A) by SUBSET_1:def 4;

        then

         A13: not x in A by XBOOLE_0:def 5;

        ((f | (A ` )) . x) = (f . x) by A12, FUNCT_1: 49;

        then ((f | (A ` )) . x) = (g . x) by A9, A12, A13;

        hence ((f | (A ` )) . x) = ((g | (A ` )) . x) by A12, FUNCT_1: 49;

      end;

      hence

       A14: (f | (A ` )) = (g | (A ` )) by A11, PARTFUN1: 5;

      

       A15: (A ` ) = (X \ A) by SUBSET_1:def 4;

      then (f | B) = ((g | (A ` )) | B) by A6, A14, XBOOLE_1: 33, RELAT_1: 74;

      then (f | B) = (g | B) by A6, A15, XBOOLE_1: 33, RELAT_1: 74;

      then

       A16: (( max+ g) | B) = ( max+ (f | B)) & (( max- g) | B) = ( max- (f | B)) by MESFUNC5: 28;

      

       A17: for r be Real holds ((A \/ B) /\ ( less_dom (g,r))) in S

      proof

        let r be Real;

        now

          let x be object;

          assume x in ((A \/ B) /\ ( less_dom (g,r)));

          then

           A18: x in ( dom f) & x in ( less_dom (g,r)) by A7, XBOOLE_0:def 4;

          then

           A19: x in ( dom g) & (g . x) < r by MESFUNC1:def 11;

           A20:

          now

            assume x in A;

            then (g . x) = +infty by A9, A18;

            hence contradiction by A19, XXREAL_0: 3;

          end;

          then

           A21: x in B by A7, A18, XBOOLE_0:def 3;

          (g . x) = (f . x) by A9, A18, A20;

          then ((f | B) . x) < r by A19, A21, FUNCT_1: 49;

          then x in ( less_dom ((f | B),r)) by A4, A5, A6, A21, MESFUNC1:def 11;

          hence x in (B /\ ( less_dom ((f | B),r))) by A21, XBOOLE_0:def 4;

        end;

        then

         A22: ((A \/ B) /\ ( less_dom (g,r))) c= (B /\ ( less_dom ((f | B),r)));

        now

          let x be object;

          assume x in (B /\ ( less_dom ((f | B),r)));

          then

           A23: x in B & x in ( less_dom ((f | B),r)) by XBOOLE_0:def 4;

          then

           A24: x in ( dom (f | B)) & ((f | B) . x) < r by MESFUNC1:def 11;

          

           A25: x in ( dom f) & not x in A by A23, A6, XBOOLE_0:def 5;

          then (g . x) = (f . x) by A9;

          then (g . x) < r by A24, FUNCT_1: 47;

          then x in ( less_dom (g,r)) by A9, A25, MESFUNC1:def 11;

          hence x in ((A \/ B) /\ ( less_dom (g,r))) by A7, A25, XBOOLE_0:def 4;

        end;

        then (B /\ ( less_dom ((f | B),r))) c= ((A \/ B) /\ ( less_dom (g,r)));

        then ((A \/ B) /\ ( less_dom (g,r))) = (B /\ ( less_dom ((f | B),r))) by A22;

        hence ((A \/ B) /\ ( less_dom (g,r))) in S by A4, A5, A6;

      end;

      then

       A26: ( max+ g) is (A \/ B) -measurable & ( max- g) is (A \/ B) -measurable by A7, A9, MESFUNC1:def 16, MESFUNC2: 25, MESFUNC2: 26;

      

       A27: (( max+ g) | B) is nonnegative & (( max- g) | B) is nonnegative by MESFUNC5: 15, MESFUN11: 5;

      

       A28: ( dom ( max+ g)) = (A \/ B) & ( dom ( max- g)) = (A \/ B) by A7, A9, MESFUNC2:def 2, MESFUNC2:def 3;

      

       A29: B = ((A \/ B) /\ B) by XBOOLE_1: 7, XBOOLE_1: 28;

      then

       A30: ( dom (( max+ g) | B)) = B & ( dom (( max- g) | B)) = B by A28, RELAT_1: 61;

      

       A31: ( max+ g) is B -measurable & ( max- g) is B -measurable by A26, XBOOLE_1: 7, MESFUNC1: 30;

      ( Integral (M,(( max+ g) | B))) = ( Integral (M,( max+ g))) & ( Integral (M,(( max- g) | B))) = ( Integral (M,( max- g))) by A2, A6, A7, A26, A28, MESFUNC5: 95;

      then ( integral+ (M,(( max+ g) | B))) = ( Integral (M,( max+ g))) & ( integral+ (M,(( max- g) | B))) = ( Integral (M,( max- g))) by A27, A28, A29, A30, A31, MESFUNC5: 42, MESFUNC5: 88;

      then ( integral+ (M,( max+ g))) < +infty & ( integral+ (M,( max- g))) < +infty by A8, A16, A26, A28, MESFUNC5: 88, MESFUN11: 5;

      hence g is_integrable_on M by A7, A9, A17, MESFUNC5:def 17, MESFUNC1:def 16;

      f is_a.e.integrable_on M by A1, A2, A3;

      then

      reconsider E = ( dom f) as Element of S by Th16;

      ( Integral (M,(f | (A ` )))) = ( Integral (M,(g | (( dom g) \ A)))) by A14, Th15;

      hence ( Integral (M,(f | (A ` )))) = ( Integral (M,g)) by A2, A7, A9, A17, MESFUNC5: 95, MESFUNC1:def 16;

    end;

    theorem :: MESFUN13:27

    for f be PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) holds ( Integral (( Prod_Measure (M1,M2)),f)) = (( Integral (M2,( Integral1 (M1,( max+ f))))) - ( Integral (M2,( Integral1 (M1,( max- f)))))) & ( Integral (( Prod_Measure (M1,M2)),f)) = (( Integral (M1,( Integral2 (M2,( max+ f))))) - ( Integral (M1,( Integral2 (M2,( max- f))))))

    proof

      let f be PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: f is_integrable_on ( Prod_Measure (M1,M2));

      set M = ( Prod_Measure (M1,M2));

      consider E be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A4: E = ( dom f) & f is E -measurable by A3, MESFUNC5:def 17;

      

       A5: ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

      

       A6: ( dom ( max+ f)) = E & ( dom ( max- f)) = E by A4, MESFUNC2:def 2, MESFUNC2:def 3;

      ( max+ f) is E -measurable & ( max- f) is E -measurable by A4, MESFUNC2: 25, MESFUNC2: 26;

      then

       A7: ( Integral (M,( max+ f))) = ( Integral (M2,( Integral1 (M1,( max+ f))))) & ( Integral (M,( max- f))) = ( Integral (M2,( Integral1 (M1,( max- f))))) & ( Integral (M,( max+ f))) = ( Integral (M1,( Integral2 (M2,( max+ f))))) & ( Integral (M,( max- f))) = ( Integral (M1,( Integral2 (M2,( max- f))))) by A1, A2, A5, A6, MESFUN12: 84;

      ( integral+ (M,( max+ f))) = ( Integral (M,( max+ f))) & ( integral+ (M,( max- f))) = ( Integral (M,( max- f))) by A4, A5, A6, MESFUNC2: 25, MESFUNC2: 26, MESFUNC5: 88;

      hence thesis by A7, MESFUNC5:def 16;

    end;

    theorem :: MESFUN13:28

    for E be Element of ( sigma ( measurable_rectangles (S1,S2))), y be Element of X2 holds ((M1 . ( Measurable-Y-section (E,y))) <> 0 implies (( Integral1 (M1,( Xchi (E, [:X1, X2:])))) . y) = +infty ) & ((M1 . ( Measurable-Y-section (E,y))) = 0 implies (( Integral1 (M1,( Xchi (E, [:X1, X2:])))) . y) = 0 )

    proof

      let E be Element of ( sigma ( measurable_rectangles (S1,S2))), y be Element of X2;

      ( ProjPMap2 (( Xchi (E, [:X1, X2:])),y)) = ( Xchi (( Y-section (E,y)),X1)) by MESFUN12: 35;

      then

       A1: (( Integral1 (M1,( Xchi (E, [:X1, X2:])))) . y) = ( Integral (M1,( Xchi (( Y-section (E,y)),X1)))) by MESFUN12:def 7;

      

       A2: ( Measurable-Y-section (E,y)) = ( Y-section (E,y)) by MEASUR11:def 7;

      hence (M1 . ( Measurable-Y-section (E,y))) <> 0 implies (( Integral1 (M1,( Xchi (E, [:X1, X2:])))) . y) = +infty by A1, MEASUR10: 33;

      assume (M1 . ( Measurable-Y-section (E,y))) = 0 ;

      hence thesis by A1, A2, MEASUR10: 33;

    end;

    theorem :: MESFUN13:29

    for E be Element of ( sigma ( measurable_rectangles (S1,S2))), x be Element of X1 holds ((M2 . ( Measurable-X-section (E,x))) <> 0 implies (( Integral2 (M2,( Xchi (E, [:X1, X2:])))) . x) = +infty ) & ((M2 . ( Measurable-X-section (E,x))) = 0 implies (( Integral2 (M2,( Xchi (E, [:X1, X2:])))) . x) = 0 )

    proof

      let E be Element of ( sigma ( measurable_rectangles (S1,S2))), x be Element of X1;

      ( ProjPMap1 (( Xchi (E, [:X1, X2:])),x)) = ( Xchi (( X-section (E,x)),X2)) by MESFUN12: 35;

      then

       A1: (( Integral2 (M2,( Xchi (E, [:X1, X2:])))) . x) = ( Integral (M2,( Xchi (( X-section (E,x)),X2)))) by MESFUN12:def 8;

      

       A2: ( Measurable-X-section (E,x)) = ( X-section (E,x)) by MEASUR11:def 6;

      hence (M2 . ( Measurable-X-section (E,x))) <> 0 implies (( Integral2 (M2,( Xchi (E, [:X1, X2:])))) . x) = +infty by A1, MEASUR10: 33;

      assume (M2 . ( Measurable-X-section (E,x))) = 0 ;

      hence thesis by A1, A2, MEASUR10: 33;

    end;

    ::$Notion-Name

    theorem :: MESFUN13:30

    for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M1 be sigma_Measure of S1, M2 be sigma_Measure of S2, f be PartFunc of [:X1, X2:], ExtREAL , SX1 be Element of S1 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) & X1 = SX1 holds ex U be Element of S1 st (M1 . U) = 0 & (for x be Element of X1 st x in (U ` ) holds ( ProjPMap1 (f,x)) is_integrable_on M2) & (( Integral2 (M2, |.f.|)) | (U ` )) is PartFunc of X1, REAL & ( Integral2 (M2,f)) is (SX1 \ U) -measurable & (( Integral2 (M2,f)) | (U ` )) is_integrable_on M1 & (( Integral2 (M2,f)) | (U ` )) in ( L1_Functions M1) & (ex g be Function of X1, ExtREAL st g is_integrable_on M1 & (g | (U ` )) = (( Integral2 (M2,f)) | (U ` )) & ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M1,g)))

    proof

      let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M1 be sigma_Measure of S1, M2 be sigma_Measure of S2, f be PartFunc of [:X1, X2:], ExtREAL , SX1 be Element of S1;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: f is_integrable_on ( Prod_Measure (M1,M2)) and

       A4: X1 = SX1;

      consider A be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A5: A = ( dom f) & f is A -measurable by A3, MESFUNC5:def 17;

      

       A6: A = ( dom |.f.|) & A = ( dom ( max+ f)) & A = ( dom ( max- f)) by A5, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;

      

       A7: |.f.| is A -measurable & ( max+ f) is A -measurable & ( max- f) is A -measurable by A5, MESFUNC2: 25, MESFUNC2: 26, MESFUNC2: 27;

      

       A8: ( Integral2 (M2, |.f.|)) is_integrable_on M1 & ( Integral2 (M2,( max+ f))) is_integrable_on M1 & ( Integral2 (M2,( max- f))) is_integrable_on M1 by A1, A2, A3, Th20;

      

       A9: ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

      ( Integral2 (M2, |.f.|)) is_a.e.finite M1 by A8, Th19;

      then

      consider U be Element of S1 such that

       A10: (M1 . U) = 0 & (( Integral2 (M2, |.f.|)) | (U ` )) is PartFunc of X1, REAL ;

      

       A11: (U ` ) = (SX1 \ U) by A4, SUBSET_1:def 4;

      then

       A12: (( Integral2 (M2, |.f.|)) | (U ` )) is_integrable_on M1 & (( Integral2 (M2,( max+ f))) | (U ` )) is_integrable_on M1 & (( Integral2 (M2,( max- f))) | (U ` )) is_integrable_on M1 by A8, MESFUNC5: 97;

      

       A13: ( dom ( Integral2 (M2,f))) = X1 & ( dom ( Integral2 (M2,( max+ f)))) = X1 & ( dom ( Integral2 (M2,( max- f)))) = X1 & ( dom ( Integral2 (M2, |.f.|))) = X1 by FUNCT_2:def 1;

      take U;

      thus (M1 . U) = 0 by A10;

      thus

       A14: for x be Element of X1 st x in (U ` ) holds ( ProjPMap1 (f,x)) is_integrable_on M2

      proof

        let x be Element of X1;

        assume

         A15: x in (U ` );

        then

         A16: x in ( dom (( Integral2 (M2, |.f.|)) | (U ` ))) by A13, RELAT_1: 57;

        ( X-section (A,x)) = ( Measurable-X-section (A,x)) by MEASUR11:def 6;

        then

         A17: ( dom ( ProjPMap1 ( |.f.|,x))) = ( Measurable-X-section (A,x)) & ( dom ( ProjPMap1 (f,x))) = ( Measurable-X-section (A,x)) by A5, A6, MESFUN12:def 3;

        

         A18: ( ProjPMap1 ( |.f.|,x)) is ( Measurable-X-section (A,x)) -measurable & ( ProjPMap1 (f,x)) is ( Measurable-X-section (A,x)) -measurable by A5, A6, A7, MESFUN12: 47;

        

         A19: ( ProjPMap1 ( |.f.|,x)) = |.( ProjPMap1 (f,x)).| by Th27;

        

        then ( integral+ (M2,( max+ ( ProjPMap1 ( |.f.|,x))))) = ( integral+ (M2,( ProjPMap1 ( |.f.|,x)))) by MESFUN11: 31

        .= ( Integral (M2,( ProjPMap1 ( |.f.|,x)))) by A6, A7, A17, A19, MESFUN12: 47, MESFUNC5: 88

        .= (( Integral2 (M2, |.f.|)) . x) by MESFUN12:def 8

        .= ((( Integral2 (M2, |.f.|)) | (U ` )) . x) by A15, FUNCT_1: 49;

        then

         A20: ( integral+ (M2,( max+ ( ProjPMap1 ( |.f.|,x))))) < +infty by A10, A16, PARTFUN1: 4, XXREAL_0: 9;

        ( integral+ (M2,( max- ( ProjPMap1 ( |.f.|,x))))) < +infty by A17, A18, A19, MESFUN11: 53;

        then |.( ProjPMap1 (f,x)).| is_integrable_on M2 by A6, A7, A17, A19, A20, MESFUN12: 47, MESFUNC5:def 17;

        hence ( ProjPMap1 (f,x)) is_integrable_on M2 by A17, A18, MESFUNC5: 100;

      end;

      thus (( Integral2 (M2, |.f.|)) | (U ` )) is PartFunc of X1, REAL by A10;

      set G1 = (( Integral2 (M2,( max+ f))) | (U ` ));

      set G2 = (( Integral2 (M2,( max- f))) | (U ` ));

      reconsider G = (G1 - G2) as PartFunc of X1, ExtREAL ;

      

       A21: ( dom G1) = (U ` ) & ( dom G2) = (U ` ) by A13, RELAT_1: 62;

       A22:

      now

        let x be object;

        per cases ;

          suppose

           A23: x in ( dom G1);

          then

          reconsider x1 = x as Element of X1;

          

           A24: (G1 . x) = (( Integral2 (M2,( max+ f))) . x) by A21, A23, FUNCT_1: 49

          .= ( Integral (M2,( ProjPMap1 (( max+ f),x1)))) by MESFUN12:def 8

          .= ( Integral (M2,( max+ ( ProjPMap1 (f,x1))))) by MESFUN12: 45;

          

           A25: ( ProjPMap1 (f,x1)) is_integrable_on M2 by A14, A21, A23;

          then

          consider B be Element of S2 such that

           A26: B = ( dom ( ProjPMap1 (f,x1))) & ( ProjPMap1 (f,x1)) is B -measurable by MESFUNC5:def 17;

          

           A27: B = ( dom ( max+ ( ProjPMap1 (f,x1)))) & ( max+ ( ProjPMap1 (f,x1))) is B -measurable by A26, MESFUNC2:def 2, MESFUN11: 10;

          ( integral+ (M2,( max+ ( ProjPMap1 (f,x1))))) < +infty by A25, MESFUNC5:def 17;

          hence (G1 . x) < +infty by A24, A27, MESFUNC5: 88, MESFUN11: 5;

        end;

          suppose not x in ( dom G1);

          hence (G1 . x) < +infty by FUNCT_1:def 2;

        end;

      end;

      now

        let x be object;

        per cases ;

          suppose

           A28: x in ( dom G1);

          then

          reconsider x1 = x as Element of X1;

          

           A29: (G1 . x) = (( Integral2 (M2,( max+ f))) . x) by A21, A28, FUNCT_1: 49

          .= ( Integral (M2,( ProjPMap1 (( max+ f),x1)))) by MESFUN12:def 8

          .= ( Integral (M2,( max+ ( ProjPMap1 (f,x1))))) by MESFUN12: 45;

          ( ProjPMap1 (f,x1)) is_integrable_on M2 by A14, A21, A28;

          then

          consider B be Element of S2 such that

           A30: B = ( dom ( ProjPMap1 (f,x1))) & ( ProjPMap1 (f,x1)) is B -measurable by MESFUNC5:def 17;

          B = ( dom ( max+ ( ProjPMap1 (f,x1)))) & ( max+ ( ProjPMap1 (f,x1))) is B -measurable by A30, MESFUNC2:def 2, MESFUN11: 10;

          hence (G1 . x) > -infty by A29, MESFUNC5: 90, MESFUN11: 5;

        end;

          suppose not x in ( dom G1);

          hence (G1 . x) > -infty by FUNCT_1:def 2;

        end;

      end;

      then

       A31: G1 is without-infty without+infty by A22, MESFUNC5:def 5, MESFUNC5:def 6;

      then

       A32: ( dom G) = (( dom G1) /\ ( dom G2)) by MESFUN11: 23;

      

       A33: ex A1 be Element of S1 st A1 = ( dom G1) & G1 is A1 -measurable by A12, MESFUNC5:def 17;

      

       A34: ex A2 be Element of S1 st A2 = ( dom G2) & G2 is A2 -measurable by A12, MESFUNC5:def 17;

      now

        let x be object;

        per cases ;

          suppose

           A35: x in ( dom G2);

          then

          reconsider x1 = x as Element of X1;

          

           A36: (G2 . x) = (( Integral2 (M2,( max- f))) . x) by A21, A35, FUNCT_1: 49

          .= ( Integral (M2,( ProjPMap1 (( max- f),x1)))) by MESFUN12:def 8

          .= ( Integral (M2,( max- ( ProjPMap1 (f,x1))))) by MESFUN12: 45;

          ( ProjPMap1 (f,x1)) is_integrable_on M2 by A14, A21, A35;

          then

          consider B be Element of S2 such that

           A37: B = ( dom ( ProjPMap1 (f,x1))) & ( ProjPMap1 (f,x1)) is B -measurable by MESFUNC5:def 17;

          B = ( dom ( max- ( ProjPMap1 (f,x1)))) & ( max- ( ProjPMap1 (f,x1))) is B -measurable by A37, MESFUNC2:def 3, MESFUN11: 10;

          hence (G2 . x) > -infty by A36, MESFUNC5: 90, MESFUN11: 5;

        end;

          suppose not x in ( dom G2);

          hence (G2 . x) > -infty by FUNCT_1:def 2;

        end;

      end;

      then G2 is without-infty by MESFUNC5:def 5;

      then

       A38: G is (SX1 \ U) -measurable by A11, A21, A31, A32, A33, A34, MEASUR11: 66;

      

       A39: ( dom (( Integral2 (M2,f)) | (U ` ))) = (U ` ) & ( dom (G | (U ` ))) = (U ` ) & ( dom (( Integral2 (M2, |.f.|)) | (U ` ))) = (U ` ) by A13, A21, A32, RELAT_1: 62;

      then

       A40: (U ` ) = ( dom ( max+ (( Integral2 (M2,f)) | (U ` )))) & (U ` ) = ( dom ( max- (( Integral2 (M2,f)) | (U ` )))) by MESFUNC2:def 2, MESFUNC2:def 3;

       A41:

      now

        let x be Element of X1;

        assume

         A42: x in ( dom (( Integral2 (M2,f)) | (U ` )));

        then

         A43: x in (U ` ) by A13, RELAT_1: 62;

        

        then

         A44: ((( Integral2 (M2,f)) | (U ` )) . x) = (( Integral2 (M2,f)) . x) by FUNCT_1: 49

        .= ( Integral (M2,( ProjPMap1 (f,x)))) by MESFUN12:def 8;

        ( X-section (A,x)) = ( Measurable-X-section (A,x)) by MEASUR11:def 6;

        then

         B17: ( dom ( ProjPMap1 ( |.f.|,x))) = ( Measurable-X-section (A,x)) & ( dom ( ProjPMap1 (f,x))) = ( Measurable-X-section (A,x)) by A5, A6, MESFUN12:def 3;

        x in ( dom G) by A21, A32, A42, RELAT_1: 57;

        

        then ((G | (U ` )) . x) = ((G1 . x) - (G2 . x)) by A21, A32, MESFUNC1:def 4

        .= ((( Integral2 (M2,( max+ f))) . x) - (G2 . x)) by A43, FUNCT_1: 49

        .= ((( Integral2 (M2,( max+ f))) . x) - (( Integral2 (M2,( max- f))) . x)) by A43, FUNCT_1: 49

        .= (( Integral (M2,( ProjPMap1 (( max+ f),x)))) - (( Integral2 (M2,( max- f))) . x)) by MESFUN12:def 8

        .= (( Integral (M2,( ProjPMap1 (( max+ f),x)))) - ( Integral (M2,( ProjPMap1 (( max- f),x))))) by MESFUN12:def 8

        .= (( Integral (M2,( max+ ( ProjPMap1 (f,x))))) - ( Integral (M2,( ProjPMap1 (( max- f),x))))) by MESFUN12: 45

        .= (( Integral (M2,( max+ ( ProjPMap1 (f,x))))) - ( Integral (M2,( max- ( ProjPMap1 (f,x)))))) by MESFUN12: 45

        .= ( Integral (M2,( ProjPMap1 (f,x)))) by A5, B17, MESFUN12: 47, MESFUN11: 54;

        hence ((( Integral2 (M2,f)) | (U ` )) . x) = ((G | (U ` )) . x) by A44;

      end;

      hence ( Integral2 (M2,f)) is (SX1 \ U) -measurable by A11, A13, A21, A32, A38, A39, PARTFUN1: 5, MESFUN12: 36;

      (( Integral2 (M2,f)) | (U ` )) is (SX1 \ U) -measurable by A13, A21, A32, A38, A41, RELAT_1: 62, PARTFUN1: 5;

      then

       A45: ( max+ (( Integral2 (M2,f)) | (U ` ))) is (SX1 \ U) -measurable & ( max- (( Integral2 (M2,f)) | (U ` ))) is (SX1 \ U) -measurable by A11, A39, MESFUNC2: 25, MESFUNC2: 26;

      now

        let y be set;

        assume y in ( rng (( Integral2 (M2,f)) | (U ` )));

        then

        consider x be Element of X1 such that

         A47: x in ( dom (( Integral2 (M2,f)) | (U ` ))) & y = ((( Integral2 (M2,f)) | (U ` )) . x) by PARTFUN1: 3;

        

         A48: x in ( dom ( Integral2 (M2,f))) & x in (U ` ) by A47, RELAT_1: 57;

        then x in ( dom (( Integral2 (M2, |.f.|)) | (U ` ))) by A13, RELAT_1: 57;

        then

         A49: ((( Integral2 (M2, |.f.|)) | (U ` )) . x) < +infty by A10, PARTFUN1: 4, XXREAL_0: 9;

        (( Integral2 (M2,f)) . x) = ( Integral (M2,( ProjPMap1 (f,x)))) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2, |.( ProjPMap1 (f,x)).|)) by A14, A48, MESFUNC5: 101;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2,( ProjPMap1 ( |.f.|,x)))) by Th27;

        then |.(( Integral2 (M2,f)) . x).| <= (( Integral2 (M2, |.f.|)) . x) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ((( Integral2 (M2, |.f.|)) | (U ` )) . x) by A48, FUNCT_1: 49;

        then |.((( Integral2 (M2,f)) | (U ` )) . x).| <= ((( Integral2 (M2, |.f.|)) | (U ` )) . x) by A47, FUNCT_1: 47;

        then |.((( Integral2 (M2,f)) | (U ` )) . x).| < +infty by A49, XXREAL_0: 2;

        hence y in REAL by A47, EXTREAL1: 41;

      end;

      then

       A50: ( rng (( Integral2 (M2,f)) | (U ` ))) c= REAL ;

      now

        let x be Element of X1;

        assume

         A51: x in ( dom ( max+ (( Integral2 (M2,f)) | (U ` ))));

        then

         A52: x in ( dom ( Integral2 (M2,f))) & x in (U ` ) by A13, A39, MESFUNC2:def 2;

        then

         A53: x in ( dom ( max+ ( Integral2 (M2,f)))) by MESFUNC2:def 2;

        

         A54: x in ( dom |.( Integral2 (M2,f)).|) by A52, MESFUNC1:def 10;

        (( max+ (( Integral2 (M2,f)) | (U ` ))) . x) = ( max (((( Integral2 (M2,f)) | (U ` )) . x), 0 )) by A51, MESFUNC2:def 2

        .= ( max ((( Integral2 (M2,f)) . x), 0 )) by A39, A40, A51, FUNCT_1: 47

        .= (( max+ ( Integral2 (M2,f))) . x) by A53, MESFUNC2:def 2;

        then (( max+ (( Integral2 (M2,f)) | (U ` ))) . x) <= ( |.( Integral2 (M2,f)).| . x) by Th29;

        then (( max+ (( Integral2 (M2,f)) | (U ` ))) . x) <= |.(( Integral2 (M2,f)) . x).| by A54, MESFUNC1:def 10;

        then

         A55: |.(( max+ (( Integral2 (M2,f)) | (U ` ))) . x).| <= |.(( Integral2 (M2,f)) . x).| by EXTREAL1: 3, MESFUNC2: 12;

        (( Integral2 (M2,f)) . x) = ( Integral (M2,( ProjPMap1 (f,x)))) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2, |.( ProjPMap1 (f,x)).|)) by A14, A40, A51, MESFUNC5: 101;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2,( ProjPMap1 ( |.f.|,x)))) by Th27;

        then |.(( Integral2 (M2,f)) . x).| <= (( Integral2 (M2, |.f.|)) . x) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ((( Integral2 (M2, |.f.|)) | (U ` )) . x) by A40, A51, FUNCT_1: 49;

        hence |.(( max+ (( Integral2 (M2,f)) | (U ` ))) . x).| <= ((( Integral2 (M2, |.f.|)) | (U ` )) . x) by A55, XXREAL_0: 2;

      end;

      then

       A56: ( max+ (( Integral2 (M2,f)) | (U ` ))) is_integrable_on M1 by A11, A12, A39, A45, A40, MESFUNC5: 102;

      now

        let x be Element of X1;

        assume

         A57: x in ( dom ( max- (( Integral2 (M2,f)) | (U ` ))));

        then

         A58: x in ( dom ( Integral2 (M2,f))) & x in (U ` ) by A13, A39, MESFUNC2:def 3;

        then

         A59: x in ( dom ( max- ( Integral2 (M2,f)))) by MESFUNC2:def 3;

        

         A60: x in ( dom |.( Integral2 (M2,f)).|) by A58, MESFUNC1:def 10;

        (( max- (( Integral2 (M2,f)) | (U ` ))) . x) = ( max (( - ((( Integral2 (M2,f)) | (U ` )) . x)), 0 )) by A57, MESFUNC2:def 3

        .= ( max (( - (( Integral2 (M2,f)) . x)), 0 )) by A39, A40, A57, FUNCT_1: 47

        .= (( max- ( Integral2 (M2,f))) . x) by A59, MESFUNC2:def 3;

        then (( max- (( Integral2 (M2,f)) | (U ` ))) . x) <= ( |.( Integral2 (M2,f)).| . x) by Th29;

        then (( max- (( Integral2 (M2,f)) | (U ` ))) . x) <= |.(( Integral2 (M2,f)) . x).| by A60, MESFUNC1:def 10;

        then

         A61: |.(( max- (( Integral2 (M2,f)) | (U ` ))) . x).| <= |.(( Integral2 (M2,f)) . x).| by EXTREAL1: 3, MESFUNC2: 13;

        (( Integral2 (M2,f)) . x) = ( Integral (M2,( ProjPMap1 (f,x)))) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2, |.( ProjPMap1 (f,x)).|)) by A14, A40, A57, MESFUNC5: 101;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2,( ProjPMap1 ( |.f.|,x)))) by Th27;

        then |.(( Integral2 (M2,f)) . x).| <= (( Integral2 (M2, |.f.|)) . x) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ((( Integral2 (M2, |.f.|)) | (U ` )) . x) by A40, A57, FUNCT_1: 49;

        hence |.(( max- (( Integral2 (M2,f)) | (U ` ))) . x).| <= ((( Integral2 (M2, |.f.|)) | (U ` )) . x) by A61, XXREAL_0: 2;

      end;

      then ( max- (( Integral2 (M2,f)) | (U ` ))) is_integrable_on M1 by A11, A12, A39, A45, A40, MESFUNC5: 102;

      then (( max+ (( Integral2 (M2,f)) | (U ` ))) - ( max- (( Integral2 (M2,f)) | (U ` )))) is_integrable_on M1 by A56, MESFUN10: 12;

      hence

       A62: (( Integral2 (M2,f)) | (U ` )) is_integrable_on M1 by MESFUNC2: 23;

      reconsider F = (( Integral2 (M2,f)) | (U ` )) as PartFunc of X1, REAL by A50, RELSET_1: 6;

      ( R_EAL F) is_integrable_on M1 by A62, MESFUNC5:def 7;

      then F is_integrable_on M1 by MESFUNC6:def 4;

      then F in { f where f be PartFunc of X1, REAL : ex ND be Element of S1 st (M1 . ND) = 0 & ( dom f) = (ND ` ) & f is_integrable_on M1 } by A10, A39;

      hence (( Integral2 (M2,f)) | (U ` )) in ( L1_Functions M1) by LPSPACE1:def 8;

      consider g1 be PartFunc of X1, ExtREAL such that

       A64: ( dom g1) = ( dom ( Integral2 (M2,( max+ f)))) & (g1 | (U ` )) = (( Integral2 (M2,( max+ f))) | (U ` )) & g1 is_integrable_on M1 & ( Integral (M1,g1)) = ( Integral (M1,(( Integral2 (M2,( max+ f))) | (U ` )))) by A8, A10, A11, A13, Th23, MESFUNC5: 97;

      consider g2 be PartFunc of X1, ExtREAL such that

       A65: ( dom g2) = ( dom ( Integral2 (M2,( max- f)))) & (g2 | (U ` )) = (( Integral2 (M2,( max- f))) | (U ` )) & g2 is_integrable_on M1 & ( Integral (M1,g2)) = ( Integral (M1,(( Integral2 (M2,( max- f))) | (U ` )))) by A8, A10, A11, A13, Th23, MESFUNC5: 97;

      consider g be PartFunc of X1, ExtREAL such that

       A66: ( dom g) = ( dom ( Integral2 (M2,f))) & (g | (U ` )) = (( Integral2 (M2,f)) | (U ` )) & g is_integrable_on M1 & ( Integral (M1,g)) = ( Integral (M1,(( Integral2 (M2,f)) | (U ` )))) by A10, A13, A62, Th23;

      reconsider g as Function of X1, ExtREAL by A13, A66, FUNCT_2:def 1;

      

       A67: ( dom (g | (U ` ))) = (( dom g) /\ (U ` )) & ( dom (g1 | (U ` ))) = (( dom g1) /\ (U ` )) & ( dom (g2 | (U ` ))) = (( dom g2) /\ (U ` )) by RELAT_1: 61;

      now

        let x be Element of X1;

        assume

         A72: x in ( dom (g2 | (U ` )));

        then

         A68: x in (U ` ) by RELAT_1: 57;

        

         A69: ( ProjPMap1 (f,x)) is_integrable_on M2 by A14, A72, RELAT_1: 57;

        then

        consider DP be Element of S2 such that

         A70: DP = ( dom ( ProjPMap1 (f,x))) & ( ProjPMap1 (f,x)) is DP -measurable by MESFUNC5:def 17;

        

         A71: DP = ( dom ( max- ( ProjPMap1 (f,x)))) & ( max- ( ProjPMap1 (f,x))) is DP -measurable by A70, MESFUNC2:def 3, MESFUNC2: 26;

        

         A73: ( max- ( ProjPMap1 (f,x))) is nonnegative by MESFUN11: 5;

        

         A74: ((g2 | (U ` )) . x) = (( Integral2 (M2,( max- f))) . x) by A65, A68, FUNCT_1: 49

        .= ( Integral (M2,( ProjPMap1 (( max- f),x)))) by MESFUN12:def 8

        .= ( Integral (M2,( max- ( ProjPMap1 (f,x))))) by MESFUN12: 45

        .= ( integral+ (M2,( max- ( ProjPMap1 (f,x))))) by A71, MESFUNC5: 88, MESFUN11: 5;

        then ((g2 | (U ` )) . x) < +infty by A69, MESFUNC5:def 17;

        hence |.((g2 | (U ` )) . x).| < +infty by A71, A73, A74, MESFUNC5: 79, EXTREAL1:def 1;

      end;

      then (g2 | (U ` )) is real-valued by MESFUNC2:def 1;

      then

       A75: ( dom ((g1 | (U ` )) - (g2 | (U ` )))) = ((( dom g1) /\ (U ` )) /\ (( dom g2) /\ (U ` ))) by A67, MESFUNC2: 2;

      then

       A76: ( dom ((g1 | (U ` )) - (g2 | (U ` )))) = ( dom (g | (U ` ))) by A13, A64, A65, A66, RELAT_1: 61;

      ( dom (g1 | (U ` ))) = (U ` ) & ( dom (g2 | (U ` ))) = (U ` ) by A13, A64, A65, RELAT_1: 62;

      then

       A77: (U ` ) = (( dom (g1 | (U ` ))) /\ ( dom (g2 | (U ` ))));

      

       A78: (g1 | (U ` )) is_integrable_on M1 & (g2 | (U ` )) is_integrable_on M1 by A11, A64, A65, MESFUNC5: 97;

      now

        let x be Element of X1;

        assume

         A79: x in ( dom (g | (U ` )));

        then

         A80: x in (U ` ) by RELAT_1: 57;

        then

         A81: ((g | (U ` )) . x) = (( Integral2 (M2,f)) . x) by A66, FUNCT_1: 49;

        ( ProjPMap1 (f,x)) is_integrable_on M2 by A14, A79, RELAT_1: 57;

        then

         A82: ex A be Element of S2 st A = ( dom ( ProjPMap1 (f,x))) & ( ProjPMap1 (f,x)) is A -measurable by MESFUNC5:def 17;

        (( Integral2 (M2,( max+ f))) . x) = ( Integral (M2,( ProjPMap1 (( max+ f),x)))) & (( Integral2 (M2,( max- f))) . x) = ( Integral (M2,( ProjPMap1 (( max- f),x)))) by MESFUN12:def 8;

        then (( Integral2 (M2,( max+ f))) . x) = ( Integral (M2,( max+ ( ProjPMap1 (f,x))))) & (( Integral2 (M2,( max- f))) . x) = ( Integral (M2,( max- ( ProjPMap1 (f,x))))) by MESFUN12: 45;

        

        then ((( Integral2 (M2,( max+ f))) . x) - (( Integral2 (M2,( max- f))) . x)) = ( Integral (M2,( ProjPMap1 (f,x)))) by A82, MESFUN11: 54

        .= (( Integral2 (M2,f)) . x) by MESFUN12:def 8;

        

        then ((g | (U ` )) . x) = (((( Integral2 (M2,( max+ f))) | (U ` )) . x) - (( Integral2 (M2,( max- f))) . x)) by A80, A81, FUNCT_1: 49

        .= (((g1 | (U ` )) . x) - ((g2 | (U ` )) . x)) by A64, A65, A80, FUNCT_1: 49;

        hence ((g | (U ` )) . x) = (((g1 | (U ` )) - (g2 | (U ` ))) . x) by A76, A79, MESFUNC1:def 4;

      end;

      then

       A83: (g | (U ` )) = ((g1 | (U ` )) - (g2 | (U ` ))) by A13, A64, A65, A66, A75, RELAT_1: 61, PARTFUN1: 5;

      

       A84: ( Integral2 (M2,( max+ f))) is SX1 -measurable & ( Integral2 (M2,( max- f))) is SX1 -measurable by A2, A6, A7, MESFUN11: 5, MESFUN12: 60;

      

       A85: ( Integral (( Prod_Measure (M1,M2)),( max+ f))) = ( Integral (M1,( Integral2 (M2,( max+ f))))) by A1, A2, A6, A7, A9, MESFUN12: 84

      .= ( Integral (M1,(( Integral2 (M2,( max+ f))) | (SX1 \ U)))) by A4, A10, A13, A84, MESFUNC5: 95

      .= ( Integral (M1,(g1 | (U ` )))) by A4, A64, SUBSET_1:def 4;

      

       A86: ( Integral (( Prod_Measure (M1,M2)),( max- f))) = ( Integral (M1,( Integral2 (M2,( max- f))))) by A1, A2, A6, A7, A9, MESFUN12: 84

      .= ( Integral (M1,(( Integral2 (M2,( max- f))) | (SX1 \ U)))) by A4, A10, A13, A84, MESFUNC5: 95

      .= ( Integral (M1,(g2 | (U ` )))) by A4, A65, SUBSET_1:def 4;

      ( Integral (( Prod_Measure (M1,M2)),f)) = (( Integral (M1,((g1 | (U ` )) | (U ` )))) - ( Integral (M1,((g2 | (U ` )) | (U ` ))))) by A5, A85, A86, MESFUN11: 54;

      then ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M1,(g | (U ` )))) by A77, A78, A83, Th21;

      hence ex g be Function of X1, ExtREAL st g is_integrable_on M1 & (g | (U ` )) = (( Integral2 (M2,f)) | (U ` )) & ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M1,g)) by A66;

    end;

    theorem :: MESFUN13:31

    for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M1 be sigma_Measure of S1, M2 be sigma_Measure of S2, f be PartFunc of [:X1, X2:], ExtREAL , SX2 be Element of S2 st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) & X2 = SX2 holds ex V be Element of S2 st (M2 . V) = 0 & (for y be Element of X2 st y in (V ` ) holds ( ProjPMap2 (f,y)) is_integrable_on M1) & (( Integral1 (M1, |.f.|)) | (V ` )) is PartFunc of X2, REAL & ( Integral1 (M1,f)) is (SX2 \ V) -measurable & (( Integral1 (M1,f)) | (V ` )) is_integrable_on M2 & (( Integral1 (M1,f)) | (V ` )) in ( L1_Functions M2) & (ex g be Function of X2, ExtREAL st g is_integrable_on M2 & (g | (V ` )) = (( Integral1 (M1,f)) | (V ` )) & ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M2,g)))

    proof

      let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M1 be sigma_Measure of S1, M2 be sigma_Measure of S2, f be PartFunc of [:X1, X2:], ExtREAL , SX2 be Element of S2;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: f is_integrable_on ( Prod_Measure (M1,M2)) and

       A4: X2 = SX2;

      consider A be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A5: A = ( dom f) & f is A -measurable by A3, MESFUNC5:def 17;

      

       A6: A = ( dom |.f.|) & A = ( dom ( max+ f)) & A = ( dom ( max- f)) by A5, MESFUNC1:def 10, MESFUNC2:def 2, MESFUNC2:def 3;

      

       A7: |.f.| is A -measurable & ( max+ f) is A -measurable & ( max- f) is A -measurable by A5, MESFUNC2: 25, MESFUNC2: 26, MESFUNC2: 27;

      

       A8: ( Integral1 (M1, |.f.|)) is_integrable_on M2 & ( Integral1 (M1,( max+ f))) is_integrable_on M2 & ( Integral1 (M1,( max- f))) is_integrable_on M2 by A1, A2, A3, Th20;

      

       A9: ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

      ( Integral1 (M1, |.f.|)) is_a.e.finite M2 by A8, Th19;

      then

      consider V be Element of S2 such that

       A10: (M2 . V) = 0 & (( Integral1 (M1, |.f.|)) | (V ` )) is PartFunc of X2, REAL ;

      

       A11: (V ` ) = (SX2 \ V) by A4, SUBSET_1:def 4;

      then

       A12: (( Integral1 (M1, |.f.|)) | (V ` )) is_integrable_on M2 & (( Integral1 (M1,( max+ f))) | (V ` )) is_integrable_on M2 & (( Integral1 (M1,( max- f))) | (V ` )) is_integrable_on M2 by A8, MESFUNC5: 97;

      

       A13: ( dom ( Integral1 (M1,f))) = X2 & ( dom ( Integral1 (M1,( max+ f)))) = X2 & ( dom ( Integral1 (M1,( max- f)))) = X2 & ( dom ( Integral1 (M1, |.f.|))) = X2 by FUNCT_2:def 1;

      take V;

      thus (M2 . V) = 0 by A10;

      thus

       A14: for y be Element of X2 st y in (V ` ) holds ( ProjPMap2 (f,y)) is_integrable_on M1

      proof

        let y be Element of X2;

        assume

         A15: y in (V ` );

        then

         A16: y in ( dom (( Integral1 (M1, |.f.|)) | (V ` ))) by A13, RELAT_1: 57;

        ( Y-section (A,y)) = ( Measurable-Y-section (A,y)) by MEASUR11:def 7;

        then

         A17: ( dom ( ProjPMap2 ( |.f.|,y))) = ( Measurable-Y-section (A,y)) & ( dom ( ProjPMap2 (f,y))) = ( Measurable-Y-section (A,y)) by A5, A6, MESFUN12:def 4;

        

         A18: ( ProjPMap2 ( |.f.|,y)) is ( Measurable-Y-section (A,y)) -measurable & ( ProjPMap2 (f,y)) is ( Measurable-Y-section (A,y)) -measurable by A5, A6, A7, MESFUN12: 47;

        

         A19: ( ProjPMap2 ( |.f.|,y)) = |.( ProjPMap2 (f,y)).| by Th27;

        

        then ( integral+ (M1,( max+ ( ProjPMap2 ( |.f.|,y))))) = ( integral+ (M1,( ProjPMap2 ( |.f.|,y)))) by MESFUN11: 31

        .= ( Integral (M1,( ProjPMap2 ( |.f.|,y)))) by A6, A7, A17, A19, MESFUN12: 47, MESFUNC5: 88

        .= (( Integral1 (M1, |.f.|)) . y) by MESFUN12:def 7

        .= ((( Integral1 (M1, |.f.|)) | (V ` )) . y) by A15, FUNCT_1: 49;

        then

         A20: ( integral+ (M1,( max+ ( ProjPMap2 ( |.f.|,y))))) < +infty by A10, A16, PARTFUN1: 4, XXREAL_0: 9;

        ( integral+ (M1,( max- ( ProjPMap2 ( |.f.|,y))))) < +infty by A17, A18, A19, MESFUN11: 53;

        then |.( ProjPMap2 (f,y)).| is_integrable_on M1 by A6, A7, A17, A19, A20, MESFUN12: 47, MESFUNC5:def 17;

        hence ( ProjPMap2 (f,y)) is_integrable_on M1 by A17, A18, MESFUNC5: 100;

      end;

      thus (( Integral1 (M1, |.f.|)) | (V ` )) is PartFunc of X2, REAL by A10;

      set G1 = (( Integral1 (M1,( max+ f))) | (V ` ));

      set G2 = (( Integral1 (M1,( max- f))) | (V ` ));

      reconsider G = (G1 - G2) as PartFunc of X2, ExtREAL ;

      

       A21: ( dom G1) = (V ` ) & ( dom G2) = (V ` ) by A13, RELAT_1: 62;

       A22:

      now

        let x be object;

        per cases ;

          suppose

           A23: x in ( dom G1);

          then

          reconsider x1 = x as Element of X2;

          

           A24: (G1 . x) = (( Integral1 (M1,( max+ f))) . x) by A21, A23, FUNCT_1: 49

          .= ( Integral (M1,( ProjPMap2 (( max+ f),x1)))) by MESFUN12:def 7

          .= ( Integral (M1,( max+ ( ProjPMap2 (f,x1))))) by MESFUN12: 46;

          

           A25: ( ProjPMap2 (f,x1)) is_integrable_on M1 by A14, A21, A23;

          then

          consider B be Element of S1 such that

           A26: B = ( dom ( ProjPMap2 (f,x1))) & ( ProjPMap2 (f,x1)) is B -measurable by MESFUNC5:def 17;

          

           A27: B = ( dom ( max+ ( ProjPMap2 (f,x1)))) & ( max+ ( ProjPMap2 (f,x1))) is B -measurable by A26, MESFUNC2:def 2, MESFUN11: 10;

          ( integral+ (M1,( max+ ( ProjPMap2 (f,x1))))) < +infty by A25, MESFUNC5:def 17;

          hence (G1 . x) < +infty by A24, A27, MESFUNC5: 88, MESFUN11: 5;

        end;

          suppose not x in ( dom G1);

          hence (G1 . x) < +infty by FUNCT_1:def 2;

        end;

      end;

      now

        let x be object;

        per cases ;

          suppose

           A28: x in ( dom G1);

          then

          reconsider x1 = x as Element of X2;

          

           A29: (G1 . x) = (( Integral1 (M1,( max+ f))) . x) by A21, A28, FUNCT_1: 49

          .= ( Integral (M1,( ProjPMap2 (( max+ f),x1)))) by MESFUN12:def 7

          .= ( Integral (M1,( max+ ( ProjPMap2 (f,x1))))) by MESFUN12: 46;

          ( ProjPMap2 (f,x1)) is_integrable_on M1 by A14, A21, A28;

          then

          consider B be Element of S1 such that

           A30: B = ( dom ( ProjPMap2 (f,x1))) & ( ProjPMap2 (f,x1)) is B -measurable by MESFUNC5:def 17;

          B = ( dom ( max+ ( ProjPMap2 (f,x1)))) & ( max+ ( ProjPMap2 (f,x1))) is B -measurable by A30, MESFUNC2:def 2, MESFUN11: 10;

          hence (G1 . x) > -infty by A29, MESFUNC5: 90, MESFUN11: 5;

        end;

          suppose not x in ( dom G1);

          hence (G1 . x) > -infty by FUNCT_1:def 2;

        end;

      end;

      then

       A31: G1 is without-infty without+infty by A22, MESFUNC5:def 5, MESFUNC5:def 6;

      then

       A32: ( dom G) = (( dom G1) /\ ( dom G2)) by MESFUN11: 23;

      

       A33: ex A1 be Element of S2 st A1 = ( dom G1) & G1 is A1 -measurable by A12, MESFUNC5:def 17;

      

       A34: ex A2 be Element of S2 st A2 = ( dom G2) & G2 is A2 -measurable by A12, MESFUNC5:def 17;

      now

        let x be object;

        per cases ;

          suppose

           A35: x in ( dom G2);

          then

          reconsider x1 = x as Element of X2;

          

           A36: (G2 . x) = (( Integral1 (M1,( max- f))) . x) by A21, A35, FUNCT_1: 49

          .= ( Integral (M1,( ProjPMap2 (( max- f),x1)))) by MESFUN12:def 7

          .= ( Integral (M1,( max- ( ProjPMap2 (f,x1))))) by MESFUN12: 46;

          ( ProjPMap2 (f,x1)) is_integrable_on M1 by A14, A21, A35;

          then

          consider B be Element of S1 such that

           A37: B = ( dom ( ProjPMap2 (f,x1))) & ( ProjPMap2 (f,x1)) is B -measurable by MESFUNC5:def 17;

          B = ( dom ( max- ( ProjPMap2 (f,x1)))) & ( max- ( ProjPMap2 (f,x1))) is B -measurable by A37, MESFUNC2:def 3, MESFUN11: 10;

          hence (G2 . x) > -infty by A36, MESFUNC5: 90, MESFUN11: 5;

        end;

          suppose not x in ( dom G2);

          hence (G2 . x) > -infty by FUNCT_1:def 2;

        end;

      end;

      then G2 is without-infty by MESFUNC5:def 5;

      then

       A38: G is (SX2 \ V) -measurable by A11, A21, A31, A32, A33, A34, MEASUR11: 66;

      

       A39: ( dom (( Integral1 (M1,f)) | (V ` ))) = (V ` ) & ( dom (G | (V ` ))) = (V ` ) & ( dom (( Integral1 (M1, |.f.|)) | (V ` ))) = (V ` ) by A13, A21, A32, RELAT_1: 62;

      then

       A40: (V ` ) = ( dom ( max+ (( Integral1 (M1,f)) | (V ` )))) & (V ` ) = ( dom ( max- (( Integral1 (M1,f)) | (V ` )))) by MESFUNC2:def 2, MESFUNC2:def 3;

       A41:

      now

        let x be Element of X2;

        assume

         A42: x in ( dom (( Integral1 (M1,f)) | (V ` )));

        then

         A43: x in (V ` ) by A13, RELAT_1: 62;

        

        then

         A44: ((( Integral1 (M1,f)) | (V ` )) . x) = (( Integral1 (M1,f)) . x) by FUNCT_1: 49

        .= ( Integral (M1,( ProjPMap2 (f,x)))) by MESFUN12:def 7;

        ( Y-section (A,x)) = ( Measurable-Y-section (A,x)) by MEASUR11:def 7;

        then

         B17: ( dom ( ProjPMap2 ( |.f.|,x))) = ( Measurable-Y-section (A,x)) & ( dom ( ProjPMap2 (f,x))) = ( Measurable-Y-section (A,x)) by A5, A6, MESFUN12:def 4;

        x in ( dom G) by A21, A32, A42, RELAT_1: 57;

        

        then ((G | (V ` )) . x) = ((G1 . x) - (G2 . x)) by A21, A32, MESFUNC1:def 4

        .= ((( Integral1 (M1,( max+ f))) . x) - (G2 . x)) by A43, FUNCT_1: 49

        .= ((( Integral1 (M1,( max+ f))) . x) - (( Integral1 (M1,( max- f))) . x)) by A43, FUNCT_1: 49

        .= (( Integral (M1,( ProjPMap2 (( max+ f),x)))) - (( Integral1 (M1,( max- f))) . x)) by MESFUN12:def 7

        .= (( Integral (M1,( ProjPMap2 (( max+ f),x)))) - ( Integral (M1,( ProjPMap2 (( max- f),x))))) by MESFUN12:def 7

        .= (( Integral (M1,( max+ ( ProjPMap2 (f,x))))) - ( Integral (M1,( ProjPMap2 (( max- f),x))))) by MESFUN12: 46

        .= (( Integral (M1,( max+ ( ProjPMap2 (f,x))))) - ( Integral (M1,( max- ( ProjPMap2 (f,x)))))) by MESFUN12: 46

        .= ( Integral (M1,( ProjPMap2 (f,x)))) by A5, B17, MESFUN12: 47, MESFUN11: 54;

        hence ((( Integral1 (M1,f)) | (V ` )) . x) = ((G | (V ` )) . x) by A44;

      end;

      hence ( Integral1 (M1,f)) is (SX2 \ V) -measurable by A11, A13, A21, A32, A38, A39, PARTFUN1: 5, MESFUN12: 36;

      (( Integral1 (M1,f)) | (V ` )) is (SX2 \ V) -measurable by A13, A21, A32, A38, A41, RELAT_1: 62, PARTFUN1: 5;

      then

       A45: ( max+ (( Integral1 (M1,f)) | (V ` ))) is (SX2 \ V) -measurable & ( max- (( Integral1 (M1,f)) | (V ` ))) is (SX2 \ V) -measurable by A11, A39, MESFUNC2: 25, MESFUNC2: 26;

      now

        let y be set;

        assume y in ( rng (( Integral1 (M1,f)) | (V ` )));

        then

        consider x be Element of X2 such that

         A47: x in ( dom (( Integral1 (M1,f)) | (V ` ))) & y = ((( Integral1 (M1,f)) | (V ` )) . x) by PARTFUN1: 3;

        

         A48: x in ( dom ( Integral1 (M1,f))) & x in (V ` ) by A47, RELAT_1: 57;

        then x in ( dom (( Integral1 (M1, |.f.|)) | (V ` ))) by A13, RELAT_1: 57;

        then

         A49: ((( Integral1 (M1, |.f.|)) | (V ` )) . x) < +infty by A10, PARTFUN1: 4, XXREAL_0: 9;

        (( Integral1 (M1,f)) . x) = ( Integral (M1,( ProjPMap2 (f,x)))) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1, |.( ProjPMap2 (f,x)).|)) by A14, A48, MESFUNC5: 101;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1,( ProjPMap2 ( |.f.|,x)))) by Th27;

        then |.(( Integral1 (M1,f)) . x).| <= (( Integral1 (M1, |.f.|)) . x) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ((( Integral1 (M1, |.f.|)) | (V ` )) . x) by A48, FUNCT_1: 49;

        then |.((( Integral1 (M1,f)) | (V ` )) . x).| <= ((( Integral1 (M1, |.f.|)) | (V ` )) . x) by A47, FUNCT_1: 47;

        then |.((( Integral1 (M1,f)) | (V ` )) . x).| < +infty by A49, XXREAL_0: 2;

        hence y in REAL by A47, EXTREAL1: 41;

      end;

      then

       A50: ( rng (( Integral1 (M1,f)) | (V ` ))) c= REAL ;

      now

        let x be Element of X2;

        assume

         A51: x in ( dom ( max+ (( Integral1 (M1,f)) | (V ` ))));

        then

         A52: x in ( dom ( Integral1 (M1,f))) & x in (V ` ) by A13, A39, MESFUNC2:def 2;

        then

         A53: x in ( dom ( max+ ( Integral1 (M1,f)))) by MESFUNC2:def 2;

        

         A54: x in ( dom |.( Integral1 (M1,f)).|) by A52, MESFUNC1:def 10;

        (( max+ (( Integral1 (M1,f)) | (V ` ))) . x) = ( max (((( Integral1 (M1,f)) | (V ` )) . x), 0 )) by A51, MESFUNC2:def 2

        .= ( max ((( Integral1 (M1,f)) . x), 0 )) by A39, A40, A51, FUNCT_1: 47

        .= (( max+ ( Integral1 (M1,f))) . x) by A53, MESFUNC2:def 2;

        then (( max+ (( Integral1 (M1,f)) | (V ` ))) . x) <= ( |.( Integral1 (M1,f)).| . x) by Th29;

        then (( max+ (( Integral1 (M1,f)) | (V ` ))) . x) <= |.(( Integral1 (M1,f)) . x).| by A54, MESFUNC1:def 10;

        then

         A55: |.(( max+ (( Integral1 (M1,f)) | (V ` ))) . x).| <= |.(( Integral1 (M1,f)) . x).| by EXTREAL1: 3, MESFUNC2: 12;

        (( Integral1 (M1,f)) . x) = ( Integral (M1,( ProjPMap2 (f,x)))) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1, |.( ProjPMap2 (f,x)).|)) by A14, A40, A51, MESFUNC5: 101;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1,( ProjPMap2 ( |.f.|,x)))) by Th27;

        then |.(( Integral1 (M1,f)) . x).| <= (( Integral1 (M1, |.f.|)) . x) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ((( Integral1 (M1, |.f.|)) | (V ` )) . x) by A40, A51, FUNCT_1: 49;

        hence |.(( max+ (( Integral1 (M1,f)) | (V ` ))) . x).| <= ((( Integral1 (M1, |.f.|)) | (V ` )) . x) by A55, XXREAL_0: 2;

      end;

      then

       A56: ( max+ (( Integral1 (M1,f)) | (V ` ))) is_integrable_on M2 by A11, A12, A39, A45, A40, MESFUNC5: 102;

      now

        let x be Element of X2;

        assume

         A57: x in ( dom ( max- (( Integral1 (M1,f)) | (V ` ))));

        then

         A58: x in ( dom ( Integral1 (M1,f))) & x in (V ` ) by A13, A39, MESFUNC2:def 3;

        then

         A59: x in ( dom ( max- ( Integral1 (M1,f)))) by MESFUNC2:def 3;

        

         A60: x in ( dom |.( Integral1 (M1,f)).|) by A58, MESFUNC1:def 10;

        (( max- (( Integral1 (M1,f)) | (V ` ))) . x) = ( max (( - ((( Integral1 (M1,f)) | (V ` )) . x)), 0 )) by A57, MESFUNC2:def 3

        .= ( max (( - (( Integral1 (M1,f)) . x)), 0 )) by A39, A40, A57, FUNCT_1: 47

        .= (( max- ( Integral1 (M1,f))) . x) by A59, MESFUNC2:def 3;

        then (( max- (( Integral1 (M1,f)) | (V ` ))) . x) <= ( |.( Integral1 (M1,f)).| . x) by Th29;

        then (( max- (( Integral1 (M1,f)) | (V ` ))) . x) <= |.(( Integral1 (M1,f)) . x).| by A60, MESFUNC1:def 10;

        then

         A61: |.(( max- (( Integral1 (M1,f)) | (V ` ))) . x).| <= |.(( Integral1 (M1,f)) . x).| by EXTREAL1: 3, MESFUNC2: 13;

        (( Integral1 (M1,f)) . x) = ( Integral (M1,( ProjPMap2 (f,x)))) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1, |.( ProjPMap2 (f,x)).|)) by A14, A40, A57, MESFUNC5: 101;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1,( ProjPMap2 ( |.f.|,x)))) by Th27;

        then |.(( Integral1 (M1,f)) . x).| <= (( Integral1 (M1, |.f.|)) . x) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ((( Integral1 (M1, |.f.|)) | (V ` )) . x) by A40, A57, FUNCT_1: 49;

        hence |.(( max- (( Integral1 (M1,f)) | (V ` ))) . x).| <= ((( Integral1 (M1, |.f.|)) | (V ` )) . x) by A61, XXREAL_0: 2;

      end;

      then ( max- (( Integral1 (M1,f)) | (V ` ))) is_integrable_on M2 by A11, A12, A39, A45, A40, MESFUNC5: 102;

      then (( max+ (( Integral1 (M1,f)) | (V ` ))) - ( max- (( Integral1 (M1,f)) | (V ` )))) is_integrable_on M2 by A56, MESFUN10: 12;

      hence

       A62: (( Integral1 (M1,f)) | (V ` )) is_integrable_on M2 by MESFUNC2: 23;

      reconsider F = (( Integral1 (M1,f)) | (V ` )) as PartFunc of X2, REAL by A50, RELSET_1: 6;

      ( R_EAL F) is_integrable_on M2 by A62, MESFUNC5:def 7;

      then F is_integrable_on M2 by MESFUNC6:def 4;

      then F in { f where f be PartFunc of X2, REAL : ex ND be Element of S2 st (M2 . ND) = 0 & ( dom f) = (ND ` ) & f is_integrable_on M2 } by A10, A39;

      hence (( Integral1 (M1,f)) | (V ` )) in ( L1_Functions M2) by LPSPACE1:def 8;

      consider g1 be PartFunc of X2, ExtREAL such that

       A64: ( dom g1) = ( dom ( Integral1 (M1,( max+ f)))) & (g1 | (V ` )) = (( Integral1 (M1,( max+ f))) | (V ` )) & g1 is_integrable_on M2 & ( Integral (M2,g1)) = ( Integral (M2,(( Integral1 (M1,( max+ f))) | (V ` )))) by A8, A10, A11, A13, Th23, MESFUNC5: 97;

      consider g2 be PartFunc of X2, ExtREAL such that

       A65: ( dom g2) = ( dom ( Integral1 (M1,( max- f)))) & (g2 | (V ` )) = (( Integral1 (M1,( max- f))) | (V ` )) & g2 is_integrable_on M2 & ( Integral (M2,g2)) = ( Integral (M2,(( Integral1 (M1,( max- f))) | (V ` )))) by A8, A10, A11, A13, Th23, MESFUNC5: 97;

      consider g be PartFunc of X2, ExtREAL such that

       A66: ( dom g) = ( dom ( Integral1 (M1,f))) & (g | (V ` )) = (( Integral1 (M1,f)) | (V ` )) & g is_integrable_on M2 & ( Integral (M2,g)) = ( Integral (M2,(( Integral1 (M1,f)) | (V ` )))) by A10, A13, A62, Th23;

      reconsider g as Function of X2, ExtREAL by A13, A66, FUNCT_2:def 1;

      

       A67: ( dom (g | (V ` ))) = (( dom g) /\ (V ` )) & ( dom (g1 | (V ` ))) = (( dom g1) /\ (V ` )) & ( dom (g2 | (V ` ))) = (( dom g2) /\ (V ` )) by RELAT_1: 61;

      now

        let x be Element of X2;

        assume

         A72: x in ( dom (g2 | (V ` )));

        then

         A68: x in (V ` ) by RELAT_1: 57;

        

         A69: ( ProjPMap2 (f,x)) is_integrable_on M1 by A14, A72, RELAT_1: 57;

        then

        consider DP be Element of S1 such that

         A70: DP = ( dom ( ProjPMap2 (f,x))) & ( ProjPMap2 (f,x)) is DP -measurable by MESFUNC5:def 17;

        

         A71: DP = ( dom ( max- ( ProjPMap2 (f,x)))) & ( max- ( ProjPMap2 (f,x))) is DP -measurable by A70, MESFUNC2:def 3, MESFUNC2: 26;

        

         A73: ( max- ( ProjPMap2 (f,x))) is nonnegative by MESFUN11: 5;

        

         A74: ((g2 | (V ` )) . x) = (( Integral1 (M1,( max- f))) . x) by A65, A68, FUNCT_1: 49

        .= ( Integral (M1,( ProjPMap2 (( max- f),x)))) by MESFUN12:def 7

        .= ( Integral (M1,( max- ( ProjPMap2 (f,x))))) by MESFUN12: 46

        .= ( integral+ (M1,( max- ( ProjPMap2 (f,x))))) by A71, MESFUNC5: 88, MESFUN11: 5;

        then ((g2 | (V ` )) . x) < +infty by A69, MESFUNC5:def 17;

        hence |.((g2 | (V ` )) . x).| < +infty by A71, A73, A74, MESFUNC5: 79, EXTREAL1:def 1;

      end;

      then (g2 | (V ` )) is real-valued by MESFUNC2:def 1;

      then

       A75: ( dom ((g1 | (V ` )) - (g2 | (V ` )))) = ((( dom g1) /\ (V ` )) /\ (( dom g2) /\ (V ` ))) by A67, MESFUNC2: 2;

      then

       A76: ( dom ((g1 | (V ` )) - (g2 | (V ` )))) = ( dom (g | (V ` ))) by A13, A64, A65, A66, RELAT_1: 61;

      ( dom (g1 | (V ` ))) = (V ` ) & ( dom (g2 | (V ` ))) = (V ` ) by A13, A64, A65, RELAT_1: 62;

      then

       A77: (V ` ) = (( dom (g1 | (V ` ))) /\ ( dom (g2 | (V ` ))));

      

       A78: (g1 | (V ` )) is_integrable_on M2 & (g2 | (V ` )) is_integrable_on M2 by A11, A64, A65, MESFUNC5: 97;

      now

        let x be Element of X2;

        assume

         A79: x in ( dom (g | (V ` )));

        then

         A80: x in (V ` ) by RELAT_1: 57;

        then

         A81: ((g | (V ` )) . x) = (( Integral1 (M1,f)) . x) by A66, FUNCT_1: 49;

        ( ProjPMap2 (f,x)) is_integrable_on M1 by A14, A79, RELAT_1: 57;

        then

         A82: ex A be Element of S1 st A = ( dom ( ProjPMap2 (f,x))) & ( ProjPMap2 (f,x)) is A -measurable by MESFUNC5:def 17;

        (( Integral1 (M1,( max+ f))) . x) = ( Integral (M1,( ProjPMap2 (( max+ f),x)))) & (( Integral1 (M1,( max- f))) . x) = ( Integral (M1,( ProjPMap2 (( max- f),x)))) by MESFUN12:def 7;

        then (( Integral1 (M1,( max+ f))) . x) = ( Integral (M1,( max+ ( ProjPMap2 (f,x))))) & (( Integral1 (M1,( max- f))) . x) = ( Integral (M1,( max- ( ProjPMap2 (f,x))))) by MESFUN12: 46;

        

        then ((( Integral1 (M1,( max+ f))) . x) - (( Integral1 (M1,( max- f))) . x)) = ( Integral (M1,( ProjPMap2 (f,x)))) by A82, MESFUN11: 54

        .= (( Integral1 (M1,f)) . x) by MESFUN12:def 7;

        

        then ((g | (V ` )) . x) = (((( Integral1 (M1,( max+ f))) | (V ` )) . x) - (( Integral1 (M1,( max- f))) . x)) by A80, A81, FUNCT_1: 49

        .= (((g1 | (V ` )) . x) - ((g2 | (V ` )) . x)) by A64, A65, A80, FUNCT_1: 49;

        hence ((g | (V ` )) . x) = (((g1 | (V ` )) - (g2 | (V ` ))) . x) by A76, A79, MESFUNC1:def 4;

      end;

      then

       A83: (g | (V ` )) = ((g1 | (V ` )) - (g2 | (V ` ))) by A13, A64, A65, A66, A75, RELAT_1: 61, PARTFUN1: 5;

      

       A84: ( Integral1 (M1,( max+ f))) is SX2 -measurable & ( Integral1 (M1,( max- f))) is SX2 -measurable by A1, A6, A7, MESFUN11: 5, MESFUN12: 59;

      

       A85: ( Integral (( Prod_Measure (M1,M2)),( max+ f))) = ( Integral (M2,( Integral1 (M1,( max+ f))))) by A1, A2, A6, A7, A9, MESFUN12: 84

      .= ( Integral (M2,(( Integral1 (M1,( max+ f))) | (SX2 \ V)))) by A4, A10, A13, A84, MESFUNC5: 95

      .= ( Integral (M2,(g1 | (V ` )))) by A4, A64, SUBSET_1:def 4;

      

       A86: ( Integral (( Prod_Measure (M1,M2)),( max- f))) = ( Integral (M2,( Integral1 (M1,( max- f))))) by A1, A2, A6, A7, A9, MESFUN12: 84

      .= ( Integral (M2,(( Integral1 (M1,( max- f))) | (SX2 \ V)))) by A4, A10, A13, A84, MESFUNC5: 95

      .= ( Integral (M2,(g2 | (V ` )))) by A4, A65, SUBSET_1:def 4;

      ( Integral (( Prod_Measure (M1,M2)),f)) = (( Integral (M2,((g1 | (V ` )) | (V ` )))) - ( Integral (M2,((g2 | (V ` )) | (V ` ))))) by A5, A85, A86, MESFUN11: 54;

      then ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M2,(g | (V ` )))) by A77, A78, A83, Th21;

      hence thesis by A66;

    end;

    theorem :: MESFUN13:32

    for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M1 be sigma_Measure of S1, M2 be sigma_Measure of S2, f be PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) & (for x be Element of X1 holds (( Integral2 (M2, |.f.|)) . x) < +infty ) holds (for x be Element of X1 holds ( ProjPMap1 (f,x)) is_integrable_on M2) & (for U be Element of S1 holds ( Integral2 (M2,f)) is U -measurable) & ( Integral2 (M2,f)) is_integrable_on M1 & ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M1,( Integral2 (M2,f)))) & ( Integral2 (M2,f)) in ( L1_Functions M1)

    proof

      let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M1 be sigma_Measure of S1, M2 be sigma_Measure of S2, f be PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: f is_integrable_on ( Prod_Measure (M1,M2)) and

       A4: for x be Element of X1 holds (( Integral2 (M2, |.f.|)) . x) < +infty ;

      reconsider XX1 = X1 as Element of S1 by MEASURE1: 7;

      consider A be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A5: A = ( dom f) & f is A -measurable by A3, MESFUNC5:def 17;

      

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

       A7:

      now

        let x be Element of X1;

        ( X-section (A,x)) = ( Measurable-X-section (A,x)) by MEASUR11:def 6;

        then

         A8: ( dom ( ProjPMap1 ( |.f.|,x))) = ( Measurable-X-section (A,x)) by A6, MESFUN12:def 3;

        

         A9: |.f.| is A -measurable by A5, MESFUNC2: 27;

        then

         A10: ( ProjPMap1 ( |.f.|,x)) is ( Measurable-X-section (A,x)) -measurable by A6, MESFUN12: 47;

        

         A11: ( ProjPMap1 ( |.f.|,x)) = |.( ProjPMap1 (f,x)).| by Th27;

        

        then ( integral+ (M2,( max+ ( ProjPMap1 ( |.f.|,x))))) = ( integral+ (M2,( ProjPMap1 ( |.f.|,x)))) by MESFUN11: 31

        .= ( Integral (M2,( ProjPMap1 ( |.f.|,x)))) by A6, A8, A9, A11, MESFUNC5: 88, MESFUN12: 47

        .= (( Integral2 (M2, |.f.|)) . x) by MESFUN12:def 8;

        then

         A12: ( integral+ (M2,( max+ ( ProjPMap1 ( |.f.|,x))))) < +infty by A4;

        ( integral+ (M2,( max- ( ProjPMap1 ( |.f.|,x))))) = 0 by A8, A10, A11, MESFUN11: 53;

        then

         A13: ( ProjPMap1 ( |.f.|,x)) is_integrable_on M2 by A6, A8, A9, A12, MESFUNC5:def 17, MESFUN12: 47;

        

         A14: ( dom ( ProjPMap1 (f,x))) = ( Measurable-X-section (A,x)) by A8, A11, MESFUNC1:def 10;

        ( ProjPMap1 (f,x)) is ( Measurable-X-section (A,x)) -measurable by A5, MESFUN12: 47;

        hence ( ProjPMap1 (f,x)) is_integrable_on M2 by A11, A13, A14, MESFUNC5: 100;

      end;

      hence for x be Element of X1 holds ( ProjPMap1 (f,x)) is_integrable_on M2;

      set G1 = ( Integral2 (M2,( max+ f)));

      set G2 = ( Integral2 (M2,( max- f)));

      set G = (G1 - G2);

      

       A15: ( dom G1) = X1 & ( dom G2) = X1 & ( dom ( Integral2 (M2,f))) = X1 & ( dom ( Integral2 (M2, |.f.|))) = X1 by FUNCT_2:def 1;

       A16:

      now

        let x be object;

        per cases ;

          suppose x in ( dom G1);

          then

          reconsider x1 = x as Element of X1;

          (G1 . x) = ( Integral (M2,( ProjPMap1 (( max+ f),x1)))) by MESFUN12:def 8;

          then

           A17: (G1 . x) = ( Integral (M2,( max+ ( ProjPMap1 (f,x1))))) by MESFUN12: 45;

          

           A18: ( ProjPMap1 (f,x1)) is_integrable_on M2 by A7;

          then

          consider B be Element of S2 such that

           A19: B = ( dom ( ProjPMap1 (f,x1))) & ( ProjPMap1 (f,x1)) is B -measurable by MESFUNC5:def 17;

          

           A20: B = ( dom ( max+ ( ProjPMap1 (f,x1)))) & ( max+ ( ProjPMap1 (f,x1))) is B -measurable by A19, MESFUNC2:def 2, MESFUN11: 10;

          ( integral+ (M2,( max+ ( ProjPMap1 (f,x1))))) < +infty by A18, MESFUNC5:def 17;

          hence (G1 . x) < +infty by A17, A20, MESFUNC5: 88, MESFUN11: 5;

        end;

          suppose not x in ( dom G1);

          hence (G1 . x) < +infty by FUNCT_1:def 2;

        end;

      end;

      now

        let x be object;

        per cases ;

          suppose x in ( dom G1);

          then

          reconsider x1 = x as Element of X1;

          (G1 . x) = ( Integral (M2,( ProjPMap1 (( max+ f),x1)))) by MESFUN12:def 8;

          then

           A21: (G1 . x) = ( Integral (M2,( max+ ( ProjPMap1 (f,x1))))) by MESFUN12: 45;

          ( ProjPMap1 (f,x1)) is_integrable_on M2 by A7;

          then

          consider B be Element of S2 such that

           A22: B = ( dom ( ProjPMap1 (f,x1))) & ( ProjPMap1 (f,x1)) is B -measurable by MESFUNC5:def 17;

          B = ( dom ( max+ ( ProjPMap1 (f,x1)))) & ( max+ ( ProjPMap1 (f,x1))) is B -measurable by A22, MESFUNC2:def 2, MESFUN11: 10;

          hence (G1 . x) > -infty by A21, MESFUNC5: 90, MESFUN11: 5;

        end;

          suppose not x in ( dom G1);

          hence (G1 . x) > -infty by FUNCT_1:def 2;

        end;

      end;

      then

       A23: G1 is without-infty without+infty by A16, MESFUNC5:def 5, MESFUNC5:def 6;

      then

       A24: ( dom G) = (( dom G1) /\ ( dom G2)) by MESFUN11: 23;

      

       TT: ( Integral2 (M2,( max+ f))) is_integrable_on M1 & ( Integral2 (M2,( max- f))) is_integrable_on M1 by A1, A2, A3, Th20;

      then

       A25: ex A1 be Element of S1 st A1 = ( dom ( Integral2 (M2,( max+ f)))) & ( Integral2 (M2,( max+ f))) is A1 -measurable by MESFUNC5:def 17;

      

       A26: ex A2 be Element of S1 st A2 = ( dom ( Integral2 (M2,( max- f)))) & ( Integral2 (M2,( max- f))) is A2 -measurable by TT, MESFUNC5:def 17;

      now

        let x be object;

        per cases ;

          suppose x in ( dom G2);

          then

          reconsider x1 = x as Element of X1;

          (G2 . x) = ( Integral (M2,( ProjPMap1 (( max- f),x1)))) by MESFUN12:def 8;

          then

           A27: (G2 . x) = ( Integral (M2,( max- ( ProjPMap1 (f,x1))))) by MESFUN12: 45;

          ( ProjPMap1 (f,x1)) is_integrable_on M2 by A7;

          then

          consider B be Element of S2 such that

           A28: B = ( dom ( ProjPMap1 (f,x1))) & ( ProjPMap1 (f,x1)) is B -measurable by MESFUNC5:def 17;

          B = ( dom ( max- ( ProjPMap1 (f,x1)))) & ( max- ( ProjPMap1 (f,x1))) is B -measurable by A28, MESFUNC2:def 3, MESFUN11: 10;

          hence (G2 . x) > -infty by A27, MESFUNC5: 90, MESFUN11: 5;

        end;

          suppose not x in ( dom G2);

          hence (G2 . x) > -infty by FUNCT_1:def 2;

        end;

      end;

      then G2 is without-infty by MESFUNC5:def 5;

      then

       A29: G is XX1 -measurable by A15, A23, A24, A25, A26, MEASUR11: 66;

      now

        let x be Element of X1;

        assume x in ( dom ( Integral2 (M2,f)));

        

         A30: (( Integral2 (M2,f)) . x) = ( Integral (M2,( ProjPMap1 (f,x)))) by MESFUN12:def 8;

        ( ProjPMap1 (f,x)) is_integrable_on M2 by A7;

        then

         B30: ex A be Element of S2 st A = ( dom ( ProjPMap1 (f,x))) & ( ProjPMap1 (f,x)) is A -measurable by MESFUNC5:def 17;

        (G . x) = ((G1 . x) - (G2 . x)) by A15, A24, MESFUNC1:def 4

        .= (( Integral (M2,( ProjPMap1 (( max+ f),x)))) - (( Integral2 (M2,( max- f))) . x)) by MESFUN12:def 8

        .= (( Integral (M2,( ProjPMap1 (( max+ f),x)))) - ( Integral (M2,( ProjPMap1 (( max- f),x))))) by MESFUN12:def 8

        .= (( Integral (M2,( max+ ( ProjPMap1 (f,x))))) - ( Integral (M2,( ProjPMap1 (( max- f),x))))) by MESFUN12: 45

        .= (( Integral (M2,( max+ ( ProjPMap1 (f,x))))) - ( Integral (M2,( max- ( ProjPMap1 (f,x)))))) by MESFUN12: 45;

        hence (G . x) = (( Integral2 (M2,f)) . x) by A30, B30, MESFUN11: 54;

      end;

      then

       A31: ( Integral2 (M2,f)) = G by A15, A24, PARTFUN1: 5;

      hence for U be Element of S1 holds ( Integral2 (M2,f)) is U -measurable by A29, MESFUNC1: 30;

      

       A32: X1 = ( dom ( max+ ( Integral2 (M2,f)))) & X1 = ( dom ( max- ( Integral2 (M2,f)))) by A15, MESFUNC2:def 2, MESFUNC2:def 3;

      

       A33: ( max+ ( Integral2 (M2,f))) is XX1 -measurable & ( max- ( Integral2 (M2,f))) is XX1 -measurable by A15, A29, A31, MESFUNC2: 25, MESFUNC2: 26;

      

       A34: ( Integral2 (M2, |.f.|)) is_integrable_on M1 by A1, A2, A3, Th20;

      now

        let x be Element of X1;

        assume x in ( dom ( max+ ( Integral2 (M2,f))));

        then

         A35: x in ( dom |.( Integral2 (M2,f)).|) by A15, A32, MESFUNC1:def 10;

        (( max+ ( Integral2 (M2,f))) . x) <= ( |.( Integral2 (M2,f)).| . x) by Th29;

        then (( max+ ( Integral2 (M2,f))) . x) <= |.(( Integral2 (M2,f)) . x).| by A35, MESFUNC1:def 10;

        then

         A36: |.(( max+ ( Integral2 (M2,f))) . x).| <= |.(( Integral2 (M2,f)) . x).| by EXTREAL1: 3, MESFUNC2: 12;

        (( Integral2 (M2,f)) . x) = ( Integral (M2,( ProjPMap1 (f,x)))) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2, |.( ProjPMap1 (f,x)).|)) by A7, MESFUNC5: 101;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2,( ProjPMap1 ( |.f.|,x)))) by Th27;

        then |.(( Integral2 (M2,f)) . x).| <= (( Integral2 (M2, |.f.|)) . x) by MESFUN12:def 8;

        hence |.(( max+ ( Integral2 (M2,f))) . x).| <= (( Integral2 (M2, |.f.|)) . x) by A36, XXREAL_0: 2;

      end;

      then

       A37: ( max+ ( Integral2 (M2,f))) is_integrable_on M1 by A15, A32, A33, A34, MESFUNC5: 102;

      now

        let x be Element of X1;

        assume x in ( dom ( max- ( Integral2 (M2,f))));

        then

         A38: x in ( dom |.( Integral2 (M2,f)).|) by A15, A32, MESFUNC1:def 10;

        (( max- ( Integral2 (M2,f))) . x) <= ( |.( Integral2 (M2,f)).| . x) by Th29;

        then (( max- ( Integral2 (M2,f))) . x) <= |.(( Integral2 (M2,f)) . x).| by A38, MESFUNC1:def 10;

        then

         A39: |.(( max- ( Integral2 (M2,f))) . x).| <= |.(( Integral2 (M2,f)) . x).| by EXTREAL1: 3, MESFUNC2: 13;

        (( Integral2 (M2,f)) . x) = ( Integral (M2,( ProjPMap1 (f,x)))) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2, |.( ProjPMap1 (f,x)).|)) by A7, MESFUNC5: 101;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2,( ProjPMap1 ( |.f.|,x)))) by Th27;

        then |.(( Integral2 (M2,f)) . x).| <= (( Integral2 (M2, |.f.|)) . x) by MESFUN12:def 8;

        hence |.(( max- ( Integral2 (M2,f))) . x).| <= (( Integral2 (M2, |.f.|)) . x) by A39, XXREAL_0: 2;

      end;

      then ( max- ( Integral2 (M2,f))) is_integrable_on M1 by A15, A32, A33, A34, MESFUNC5: 102;

      then (( max+ ( Integral2 (M2,f))) - ( max- ( Integral2 (M2,f)))) is_integrable_on M1 by A37, MESFUN10: 12;

      hence

       A40: ( Integral2 (M2,f)) is_integrable_on M1 by MESFUNC2: 23;

      

       A41: ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

      

       A42: ( dom ( max+ f)) = A & ( dom ( max- f)) = A by A5, MESFUNC2:def 2, MESFUNC2:def 3;

      

       A43: ( max+ f) is A -measurable & ( max- f) is A -measurable by A5, MESFUNC2: 25, MESFUNC2: 26;

      then

       A44: ( Integral (( Prod_Measure (M1,M2)),( max- f))) = ( Integral (M1,G2)) by A1, A2, A41, A42, MESFUN12: 84;

      ( Integral (( Prod_Measure (M1,M2)),f)) = (( Integral (( Prod_Measure (M1,M2)),( max+ f))) - ( Integral (( Prod_Measure (M1,M2)),( max- f)))) by A5, MESFUN11: 54

      .= (( Integral (M1,(G1 | XX1))) - ( Integral (M1,(G2 | XX1)))) by A1, A2, A41, A42, A43, A44, MESFUN12: 84;

      hence ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M1,( Integral2 (M2,f)))) by A15, A24, A31, TT, Th21;

      now

        let y be set;

        assume y in ( rng ( Integral2 (M2,f)));

        then

        consider x be Element of X1 such that

         A45: x in ( dom ( Integral2 (M2,f))) & y = (( Integral2 (M2,f)) . x) by PARTFUN1: 3;

        (( Integral2 (M2,f)) . x) = ( Integral (M2,( ProjPMap1 (f,x)))) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2, |.( ProjPMap1 (f,x)).|)) by A7, MESFUNC5: 101;

        then |.(( Integral2 (M2,f)) . x).| <= ( Integral (M2,( ProjPMap1 ( |.f.|,x)))) by Th27;

        then |.(( Integral2 (M2,f)) . x).| <= (( Integral2 (M2, |.f.|)) . x) by MESFUN12:def 8;

        then |.(( Integral2 (M2,f)) . x).| < +infty by A4, XXREAL_0: 2;

        hence y in REAL by A45, EXTREAL1: 41;

      end;

      then ( rng ( Integral2 (M2,f))) c= REAL ;

      then

      reconsider F = ( Integral2 (M2,f)) as PartFunc of X1, REAL by RELSET_1: 6;

      reconsider ND = {} as Element of S1 by MEASURE1: 7;

      

       A46: (M1 . ND) = 0 by VALUED_0:def 19;

      (ND ` ) = (X1 \ {} ) by SUBSET_1:def 4

      .= X1;

      then

       A47: ( dom F) = (ND ` ) by FUNCT_2:def 1;

      ( R_EAL F) is_integrable_on M1 by A40, MESFUNC5:def 7;

      then F is_integrable_on M1 by MESFUNC6:def 4;

      then F in { f where f be PartFunc of X1, REAL : ex ND be Element of S1 st (M1 . ND) = 0 & ( dom f) = (ND ` ) & f is_integrable_on M1 } by A46, A47;

      hence ( Integral2 (M2,f)) in ( L1_Functions M1) by LPSPACE1:def 8;

    end;

    theorem :: MESFUN13:33

    for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M1 be sigma_Measure of S1, M2 be sigma_Measure of S2, f be PartFunc of [:X1, X2:], ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is_integrable_on ( Prod_Measure (M1,M2)) & (for y be Element of X2 holds (( Integral1 (M1, |.f.|)) . y) < +infty ) holds (for y be Element of X2 holds ( ProjPMap2 (f,y)) is_integrable_on M1) & (for V be Element of S2 holds ( Integral1 (M1,f)) is V -measurable) & ( Integral1 (M1,f)) is_integrable_on M2 & ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M2,( Integral1 (M1,f)))) & ( Integral1 (M1,f)) in ( L1_Functions M2)

    proof

      let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M1 be sigma_Measure of S1, M2 be sigma_Measure of S2, f be PartFunc of [:X1, X2:], ExtREAL ;

      assume that

       A1: M1 is sigma_finite and

       A2: M2 is sigma_finite and

       A3: f is_integrable_on ( Prod_Measure (M1,M2)) and

       A4: for y be Element of X2 holds (( Integral1 (M1, |.f.|)) . y) < +infty ;

      reconsider XX2 = X2 as Element of S2 by MEASURE1: 7;

      consider A be Element of ( sigma ( measurable_rectangles (S1,S2))) such that

       A5: A = ( dom f) & f is A -measurable by A3, MESFUNC5:def 17;

      

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

       A7:

      now

        let x be Element of X2;

        ( Y-section (A,x)) = ( Measurable-Y-section (A,x)) by MEASUR11:def 7;

        then

         A8: ( dom ( ProjPMap2 ( |.f.|,x))) = ( Measurable-Y-section (A,x)) by A6, MESFUN12:def 4;

        

         A9: |.f.| is A -measurable by A5, MESFUNC2: 27;

        then

         A10: ( ProjPMap2 ( |.f.|,x)) is ( Measurable-Y-section (A,x)) -measurable by A6, MESFUN12: 47;

        

         A11: ( ProjPMap2 ( |.f.|,x)) = |.( ProjPMap2 (f,x)).| by Th27;

        

        then ( integral+ (M1,( max+ ( ProjPMap2 ( |.f.|,x))))) = ( integral+ (M1,( ProjPMap2 ( |.f.|,x)))) by MESFUN11: 31

        .= ( Integral (M1,( ProjPMap2 ( |.f.|,x)))) by A6, A8, A9, A11, MESFUNC5: 88, MESFUN12: 47

        .= (( Integral1 (M1, |.f.|)) . x) by MESFUN12:def 7;

        then

         A12: ( integral+ (M1,( max+ ( ProjPMap2 ( |.f.|,x))))) < +infty by A4;

        ( integral+ (M1,( max- ( ProjPMap2 ( |.f.|,x))))) = 0 by A8, A10, A11, MESFUN11: 53;

        then

         A13: ( ProjPMap2 ( |.f.|,x)) is_integrable_on M1 by A6, A8, A9, A12, MESFUNC5:def 17, MESFUN12: 47;

        

         A14: ( dom ( ProjPMap2 (f,x))) = ( Measurable-Y-section (A,x)) by A8, A11, MESFUNC1:def 10;

        ( ProjPMap2 (f,x)) is ( Measurable-Y-section (A,x)) -measurable by A5, MESFUN12: 47;

        hence ( ProjPMap2 (f,x)) is_integrable_on M1 by A11, A13, A14, MESFUNC5: 100;

      end;

      hence for x be Element of X2 holds ( ProjPMap2 (f,x)) is_integrable_on M1;

      set G1 = ( Integral1 (M1,( max+ f)));

      set G2 = ( Integral1 (M1,( max- f)));

      set G = (G1 - G2);

      

       A15: ( dom G1) = X2 & ( dom G2) = X2 & ( dom ( Integral1 (M1,f))) = X2 & ( dom ( Integral1 (M1, |.f.|))) = X2 by FUNCT_2:def 1;

       A16:

      now

        let x be object;

        per cases ;

          suppose x in ( dom G1);

          then

          reconsider x1 = x as Element of X2;

          (G1 . x) = ( Integral (M1,( ProjPMap2 (( max+ f),x1)))) by MESFUN12:def 7;

          then

           A17: (G1 . x) = ( Integral (M1,( max+ ( ProjPMap2 (f,x1))))) by MESFUN12: 46;

          

           A18: ( ProjPMap2 (f,x1)) is_integrable_on M1 by A7;

          then

          consider B be Element of S1 such that

           A19: B = ( dom ( ProjPMap2 (f,x1))) & ( ProjPMap2 (f,x1)) is B -measurable by MESFUNC5:def 17;

          

           A20: B = ( dom ( max+ ( ProjPMap2 (f,x1)))) & ( max+ ( ProjPMap2 (f,x1))) is B -measurable by A19, MESFUNC2:def 2, MESFUN11: 10;

          ( integral+ (M1,( max+ ( ProjPMap2 (f,x1))))) < +infty by A18, MESFUNC5:def 17;

          hence (G1 . x) < +infty by A17, A20, MESFUNC5: 88, MESFUN11: 5;

        end;

          suppose not x in ( dom G1);

          hence (G1 . x) < +infty by FUNCT_1:def 2;

        end;

      end;

      now

        let x be object;

        per cases ;

          suppose x in ( dom G1);

          then

          reconsider x1 = x as Element of X2;

          (G1 . x) = ( Integral (M1,( ProjPMap2 (( max+ f),x1)))) by MESFUN12:def 7;

          then

           A21: (G1 . x) = ( Integral (M1,( max+ ( ProjPMap2 (f,x1))))) by MESFUN12: 46;

          ( ProjPMap2 (f,x1)) is_integrable_on M1 by A7;

          then

          consider B be Element of S1 such that

           A22: B = ( dom ( ProjPMap2 (f,x1))) & ( ProjPMap2 (f,x1)) is B -measurable by MESFUNC5:def 17;

          B = ( dom ( max+ ( ProjPMap2 (f,x1)))) & ( max+ ( ProjPMap2 (f,x1))) is B -measurable by A22, MESFUNC2:def 2, MESFUN11: 10;

          hence (G1 . x) > -infty by A21, MESFUNC5: 90, MESFUN11: 5;

        end;

          suppose not x in ( dom G1);

          hence (G1 . x) > -infty by FUNCT_1:def 2;

        end;

      end;

      then

       A23: G1 is without-infty without+infty by A16, MESFUNC5:def 5, MESFUNC5:def 6;

      then

       A24: ( dom G) = (( dom G1) /\ ( dom G2)) by MESFUN11: 23;

      

       TT: ( Integral1 (M1,( max+ f))) is_integrable_on M2 & ( Integral1 (M1,( max- f))) is_integrable_on M2 by A1, A2, A3, Th20;

      then

       A25: ex A1 be Element of S2 st A1 = ( dom ( Integral1 (M1,( max+ f)))) & ( Integral1 (M1,( max+ f))) is A1 -measurable by MESFUNC5:def 17;

      

       A26: ex A2 be Element of S2 st A2 = ( dom ( Integral1 (M1,( max- f)))) & ( Integral1 (M1,( max- f))) is A2 -measurable by TT, MESFUNC5:def 17;

      now

        let x be object;

        per cases ;

          suppose x in ( dom G2);

          then

          reconsider x1 = x as Element of X2;

          (G2 . x) = ( Integral (M1,( ProjPMap2 (( max- f),x1)))) by MESFUN12:def 7;

          then

           A27: (G2 . x) = ( Integral (M1,( max- ( ProjPMap2 (f,x1))))) by MESFUN12: 46;

          ( ProjPMap2 (f,x1)) is_integrable_on M1 by A7;

          then

          consider B be Element of S1 such that

           A28: B = ( dom ( ProjPMap2 (f,x1))) & ( ProjPMap2 (f,x1)) is B -measurable by MESFUNC5:def 17;

          B = ( dom ( max- ( ProjPMap2 (f,x1)))) & ( max- ( ProjPMap2 (f,x1))) is B -measurable by A28, MESFUNC2:def 3, MESFUN11: 10;

          hence (G2 . x) > -infty by A27, MESFUNC5: 90, MESFUN11: 5;

        end;

          suppose not x in ( dom G2);

          hence (G2 . x) > -infty by FUNCT_1:def 2;

        end;

      end;

      then G2 is without-infty by MESFUNC5:def 5;

      then

       A29: G is XX2 -measurable by A15, A23, A24, A25, A26, MEASUR11: 66;

      now

        let x be Element of X2;

        assume x in ( dom ( Integral1 (M1,f)));

        

         A30: (( Integral1 (M1,f)) . x) = ( Integral (M1,( ProjPMap2 (f,x)))) by MESFUN12:def 7;

        ( ProjPMap2 (f,x)) is_integrable_on M1 by A7;

        then

         B30: ex A be Element of S1 st A = ( dom ( ProjPMap2 (f,x))) & ( ProjPMap2 (f,x)) is A -measurable by MESFUNC5:def 17;

        (G . x) = ((G1 . x) - (G2 . x)) by A15, A24, MESFUNC1:def 4

        .= (( Integral (M1,( ProjPMap2 (( max+ f),x)))) - (( Integral1 (M1,( max- f))) . x)) by MESFUN12:def 7

        .= (( Integral (M1,( ProjPMap2 (( max+ f),x)))) - ( Integral (M1,( ProjPMap2 (( max- f),x))))) by MESFUN12:def 7

        .= (( Integral (M1,( max+ ( ProjPMap2 (f,x))))) - ( Integral (M1,( ProjPMap2 (( max- f),x))))) by MESFUN12: 46

        .= (( Integral (M1,( max+ ( ProjPMap2 (f,x))))) - ( Integral (M1,( max- ( ProjPMap2 (f,x)))))) by MESFUN12: 46;

        hence (G . x) = (( Integral1 (M1,f)) . x) by A30, B30, MESFUN11: 54;

      end;

      then

       A31: ( Integral1 (M1,f)) = G by A15, A24, PARTFUN1: 5;

      hence for V be Element of S2 holds ( Integral1 (M1,f)) is V -measurable by A29, MESFUNC1: 30;

      

       A32: X2 = ( dom ( max+ ( Integral1 (M1,f)))) & X2 = ( dom ( max- ( Integral1 (M1,f)))) by A15, MESFUNC2:def 2, MESFUNC2:def 3;

      

       A33: ( max+ ( Integral1 (M1,f))) is XX2 -measurable & ( max- ( Integral1 (M1,f))) is XX2 -measurable by A15, A29, A31, MESFUNC2: 25, MESFUNC2: 26;

      

       A34: ( Integral1 (M1, |.f.|)) is_integrable_on M2 by A1, A2, A3, Th20;

      now

        let x be Element of X2;

        assume x in ( dom ( max+ ( Integral1 (M1,f))));

        then

         A35: x in ( dom |.( Integral1 (M1,f)).|) by A15, A32, MESFUNC1:def 10;

        (( max+ ( Integral1 (M1,f))) . x) <= ( |.( Integral1 (M1,f)).| . x) by Th29;

        then (( max+ ( Integral1 (M1,f))) . x) <= |.(( Integral1 (M1,f)) . x).| by A35, MESFUNC1:def 10;

        then

         A36: |.(( max+ ( Integral1 (M1,f))) . x).| <= |.(( Integral1 (M1,f)) . x).| by EXTREAL1: 3, MESFUNC2: 12;

        (( Integral1 (M1,f)) . x) = ( Integral (M1,( ProjPMap2 (f,x)))) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1, |.( ProjPMap2 (f,x)).|)) by A7, MESFUNC5: 101;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1,( ProjPMap2 ( |.f.|,x)))) by Th27;

        then |.(( Integral1 (M1,f)) . x).| <= (( Integral1 (M1, |.f.|)) . x) by MESFUN12:def 7;

        hence |.(( max+ ( Integral1 (M1,f))) . x).| <= (( Integral1 (M1, |.f.|)) . x) by A36, XXREAL_0: 2;

      end;

      then

       A37: ( max+ ( Integral1 (M1,f))) is_integrable_on M2 by A15, A32, A33, A34, MESFUNC5: 102;

      now

        let x be Element of X2;

        assume x in ( dom ( max- ( Integral1 (M1,f))));

        then

         A38: x in ( dom |.( Integral1 (M1,f)).|) by A15, A32, MESFUNC1:def 10;

        (( max- ( Integral1 (M1,f))) . x) <= ( |.( Integral1 (M1,f)).| . x) by Th29;

        then (( max- ( Integral1 (M1,f))) . x) <= |.(( Integral1 (M1,f)) . x).| by A38, MESFUNC1:def 10;

        then

         A39: |.(( max- ( Integral1 (M1,f))) . x).| <= |.(( Integral1 (M1,f)) . x).| by EXTREAL1: 3, MESFUNC2: 13;

        (( Integral1 (M1,f)) . x) = ( Integral (M1,( ProjPMap2 (f,x)))) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1, |.( ProjPMap2 (f,x)).|)) by A7, MESFUNC5: 101;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1,( ProjPMap2 ( |.f.|,x)))) by Th27;

        then |.(( Integral1 (M1,f)) . x).| <= (( Integral1 (M1, |.f.|)) . x) by MESFUN12:def 7;

        hence |.(( max- ( Integral1 (M1,f))) . x).| <= (( Integral1 (M1, |.f.|)) . x) by A39, XXREAL_0: 2;

      end;

      then ( max- ( Integral1 (M1,f))) is_integrable_on M2 by A15, A32, A33, A34, MESFUNC5: 102;

      then (( max+ ( Integral1 (M1,f))) - ( max- ( Integral1 (M1,f)))) is_integrable_on M2 by A37, MESFUN10: 12;

      hence

       A40: ( Integral1 (M1,f)) is_integrable_on M2 by MESFUNC2: 23;

      

       A41: ( max+ f) is nonnegative & ( max- f) is nonnegative by MESFUN11: 5;

      

       A42: ( dom ( max+ f)) = A & ( dom ( max- f)) = A by A5, MESFUNC2:def 2, MESFUNC2:def 3;

      

       A43: ( max+ f) is A -measurable & ( max- f) is A -measurable by A5, MESFUNC2: 25, MESFUNC2: 26;

      then

       A44: ( Integral (( Prod_Measure (M1,M2)),( max- f))) = ( Integral (M2,G2)) by A1, A2, A41, A42, MESFUN12: 84;

      ( Integral (( Prod_Measure (M1,M2)),f)) = (( Integral (( Prod_Measure (M1,M2)),( max+ f))) - ( Integral (( Prod_Measure (M1,M2)),( max- f)))) by A5, MESFUN11: 54

      .= (( Integral (M2,(G1 | XX2))) - ( Integral (M2,(G2 | XX2)))) by A1, A2, A41, A42, A43, A44, MESFUN12: 84;

      hence ( Integral (( Prod_Measure (M1,M2)),f)) = ( Integral (M2,( Integral1 (M1,f)))) by A15, A24, A31, TT, Th21;

      now

        let y be set;

        assume y in ( rng ( Integral1 (M1,f)));

        then

        consider x be Element of X2 such that

         A45: x in ( dom ( Integral1 (M1,f))) & y = (( Integral1 (M1,f)) . x) by PARTFUN1: 3;

        (( Integral1 (M1,f)) . x) = ( Integral (M1,( ProjPMap2 (f,x)))) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1, |.( ProjPMap2 (f,x)).|)) by A7, MESFUNC5: 101;

        then |.(( Integral1 (M1,f)) . x).| <= ( Integral (M1,( ProjPMap2 ( |.f.|,x)))) by Th27;

        then |.(( Integral1 (M1,f)) . x).| <= (( Integral1 (M1, |.f.|)) . x) by MESFUN12:def 7;

        then |.(( Integral1 (M1,f)) . x).| < +infty by A4, XXREAL_0: 2;

        hence y in REAL by A45, EXTREAL1: 41;

      end;

      then ( rng ( Integral1 (M1,f))) c= REAL ;

      then

      reconsider F = ( Integral1 (M1,f)) as PartFunc of X2, REAL by RELSET_1: 6;

      reconsider ND = {} as Element of S2 by MEASURE1: 7;

      

       A46: (M2 . ND) = 0 by VALUED_0:def 19;

      (ND ` ) = (X2 \ {} ) by SUBSET_1:def 4

      .= X2;

      then

       A47: ( dom F) = (ND ` ) by FUNCT_2:def 1;

      ( R_EAL F) is_integrable_on M2 by A40, MESFUNC5:def 7;

      then F is_integrable_on M2 by MESFUNC6:def 4;

      then F in { f where f be PartFunc of X2, REAL : ex ND be Element of S2 st (M2 . ND) = 0 & ( dom f) = (ND ` ) & f is_integrable_on M2 } by A46, A47;

      hence ( Integral1 (M1,f)) in ( L1_Functions M2) by LPSPACE1:def 8;

    end;