measur10.miz



    begin

    theorem :: MEASUR10:1

    

     Th23: for A,A1,A2,B,B1,B2 be non empty set holds [:A1, B1:] misses [:A2, B2:] & [:A, B:] = ( [:A1, B1:] \/ [:A2, B2:]) iff (A1 misses A2 & A = (A1 \/ A2) & B = B1 & B = B2) or (B1 misses B2 & B = (B1 \/ B2) & A = A1 & A = A2)

    proof

      let A,A1,A2,B,B1,B2 be non empty set;

      hereby

        assume

         A2: [:A1, B1:] misses [:A2, B2:] & [:A, B:] = ( [:A1, B1:] \/ [:A2, B2:]);

         [:A1, B1:] c= [:A, B:] & [:A2, B2:] c= [:A, B:] by A2, XBOOLE_1: 7;

        then

         A3: A1 c= A & B1 c= B & A2 c= A & B2 c= B by ZFMISC_1: 114;

         [:(A1 \/ A2), (B1 \/ B2):] = ((( [:A1, B1:] \/ [:A1, B2:]) \/ [:A2, B1:]) \/ [:A2, B2:]) by ZFMISC_1: 98

        .= ((( [:A1, B1:] \/ [:A1, B2:]) \/ [:A2, B2:]) \/ [:A2, B1:]) by XBOOLE_1: 4

        .= (( [:A1, B1:] \/ ( [:A2, B2:] \/ [:A1, B2:])) \/ [:A2, B1:]) by XBOOLE_1: 4

        .= ((( [:A1, B1:] \/ [:A2, B2:]) \/ [:A1, B2:]) \/ [:A2, B1:]) by XBOOLE_1: 4

        .= (( [:A1, B1:] \/ [:A2, B2:]) \/ ( [:A1, B2:] \/ [:A2, B1:])) by XBOOLE_1: 4;

        then

         A5: ( [:A1, B1:] \/ [:A2, B2:]) c= [:(A1 \/ A2), (B1 \/ B2):] by XBOOLE_1: 7;

        

         A6: [:(A1 /\ A2), (B1 /\ B2):] = {} by A2, ZFMISC_1: 100;

        per cases by A6;

          suppose

           A7: (A1 /\ A2) = {} ;

          then

           B7: A1 misses A2;

           A12:

          now

            assume (B \ B1) <> {} ;

            then

            consider y be object such that

             A8: y in (B \ B1) by XBOOLE_0:def 1;

            

             A9: y in B & not y in B1 by A8, XBOOLE_0:def 5;

            consider x be object such that

             A10: x in A1 by XBOOLE_0:def 1;

            

             A11: [x, y] in [:A, B:] by A3, A10, A8, ZFMISC_1:def 2;

             not x in A2 by B7, A10, XBOOLE_0: 3;

            then not [x, y] in [:A1, B1:] & not [x, y] in [:A2, B2:] by A9, ZFMISC_1: 87;

            hence contradiction by A11, A2, XBOOLE_0:def 3;

          end;

          now

            assume (B \ B2) <> {} ;

            then

            consider y be object such that

             A14: y in (B \ B2) by XBOOLE_0:def 1;

            

             A15: y in B & not y in B2 by A14, XBOOLE_0:def 5;

            consider x be object such that

             A16: x in A2 by XBOOLE_0:def 1;

            

             A17: [x, y] in [:A, B:] by A3, A16, A14, ZFMISC_1:def 2;

             not x in A1 by B7, A16, XBOOLE_0: 3;

            then not [x, y] in [:A1, B1:] & not [x, y] in [:A2, B2:] by A15, ZFMISC_1: 87;

            hence contradiction by A17, A2, XBOOLE_0:def 3;

          end;

          hence (A1 misses A2 & A = (A1 \/ A2) & B = B1 & B = B2) or (B1 misses B2 & B = (B1 \/ B2) & A = A1 & A = A2) by A3, A5, A7, A12, XBOOLE_1: 8, XBOOLE_1: 37, A2, ZFMISC_1: 114;

        end;

          suppose

           A18: (B1 /\ B2) = {} ;

          then

           B18: B1 misses B2;

           A19:

          now

            assume (A \ A1) <> {} ;

            then

            consider x be object such that

             A20: x in (A \ A1) by XBOOLE_0:def 1;

            

             A21: x in A & not x in A1 by A20, XBOOLE_0:def 5;

            consider y be object such that

             A22: y in B1 by XBOOLE_0:def 1;

            

             A23: [x, y] in [:A, B:] by A3, A22, A20, ZFMISC_1:def 2;

             not y in B2 by B18, A22, XBOOLE_0: 3;

            then not [x, y] in [:A1, B1:] & not [x, y] in [:A2, B2:] by A21, ZFMISC_1: 87;

            hence contradiction by A23, A2, XBOOLE_0:def 3;

          end;

          now

            assume (A \ A2) <> {} ;

            then

            consider x be object such that

             A24: x in (A \ A2) by XBOOLE_0:def 1;

            

             A25: x in A & not x in A2 by A24, XBOOLE_0:def 5;

            consider y be object such that

             A26: y in B2 by XBOOLE_0:def 1;

            

             A27: [x, y] in [:A, B:] by A3, A26, A24, ZFMISC_1:def 2;

             not y in B1 by B18, A26, XBOOLE_0: 3;

            then not [x, y] in [:A1, B1:] & not [x, y] in [:A2, B2:] by A25, ZFMISC_1: 87;

            hence contradiction by A27, A2, XBOOLE_0:def 3;

          end;

          hence (A1 misses A2 & A = (A1 \/ A2) & B = B1 & B = B2) or (B1 misses B2 & B = (B1 \/ B2) & A = A1 & A = A2) by A3, A5, A18, A19, XBOOLE_1: 8, XBOOLE_1: 37, A2, ZFMISC_1: 114;

        end;

      end;

      assume

       A28: (A1 misses A2 & A = (A1 \/ A2) & B = B1 & B = B2) or (B1 misses B2 & B = (B1 \/ B2) & A = A1 & A = A2);

      per cases by A28;

        suppose

         A29: A1 misses A2 & A = (A1 \/ A2) & B = B1 & B = B2;

        for z be object holds not z in ( [:A1, B1:] /\ [:A2, B2:])

        proof

          let z be object;

          assume z in ( [:A1, B1:] /\ [:A2, B2:]);

          then

           A31: z in [:A1, B1:] & z in [:A2, B2:] by XBOOLE_0:def 4;

          then

          consider x,y be object such that

           A32: x in A1 & y in B1 & z = [x, y] by ZFMISC_1: 84;

          x in A2 & y in B2 by A31, A32, ZFMISC_1: 87;

          hence contradiction by A32, A29, XBOOLE_0: 3;

        end;

        hence [:A1, B1:] misses [:A2, B2:] & [:A, B:] = ( [:A1, B1:] \/ [:A2, B2:]) by A29, ZFMISC_1: 97, XBOOLE_0: 4;

      end;

        suppose

         A33: B1 misses B2 & B = (B1 \/ B2) & A = A1 & A = A2;

        for z be object holds not z in ( [:A1, B1:] /\ [:A2, B2:])

        proof

          let z be object;

          assume z in ( [:A1, B1:] /\ [:A2, B2:]);

          then

           A35: z in [:A1, B1:] & z in [:A2, B2:] by XBOOLE_0:def 4;

          then

          consider x,y be object such that

           A36: x in A1 & y in B1 & z = [x, y] by ZFMISC_1: 84;

          x in A2 & y in B2 by A35, A36, ZFMISC_1: 87;

          hence contradiction by A36, A33, XBOOLE_0: 3;

        end;

        hence [:A1, B1:] misses [:A2, B2:] & [:A, B:] = ( [:A1, B1:] \/ [:A2, B2:]) by A33, ZFMISC_1: 97, XBOOLE_0: 4;

      end;

    end;

    definition

      let C,D be non empty set, F be sequence of ( Funcs (C,D)), n be Nat;

      :: original: .

      redefine

      func F . n -> Function of C, D ;

      correctness

      proof

        (F . n) in ( Funcs (C,D));

        hence thesis by FUNCT_2: 66;

      end;

    end

    theorem :: MEASUR10:2

    

     Th26: for X,Y,A,B be set, x,y be object st x in X & y in Y holds ((( chi (A,X)) . x) * (( chi (B,Y)) . y)) = (( chi ( [:A, B:], [:X, Y:])) . (x,y))

    proof

      let X,Y,A,B be set, x,y be object;

      assume

       A1: x in X & y in Y;

      per cases ;

        suppose

         A2: x in A & y in B;

        then

         A3: [x, y] in [:X, Y:] & [x, y] in [:A, B:] by A1, ZFMISC_1: 87;

        (( chi (A,X)) . x) = 1 & (( chi (B,Y)) . y) = 1 by A1, A2, FUNCT_3:def 3;

        then ((( chi (A,X)) . x) * (( chi (B,Y)) . y)) = (1 * 1) by XXREAL_3:def 5;

        hence ((( chi (A,X)) . x) * (( chi (B,Y)) . y)) = (( chi ( [:A, B:], [:X, Y:])) . (x,y)) by A3, FUNCT_3:def 3;

      end;

        suppose

         A4: not x in A or not y in B;

        then not [x, y] in [:A, B:] & [x, y] in [:X, Y:] by A1, ZFMISC_1: 87;

        then

         A5: (( chi ( [:A, B:], [:X, Y:])) . (x,y)) = 0 by FUNCT_3:def 3;

        per cases by A4;

          suppose not x in A;

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

          hence ((( chi (A,X)) . x) * (( chi (B,Y)) . y)) = (( chi ( [:A, B:], [:X, Y:])) . (x,y)) by A5;

        end;

          suppose not y in B;

          then (( chi (B,Y)) . y) = 0 by A1, FUNCT_3:def 3;

          hence ((( chi (A,X)) . x) * (( chi (B,Y)) . y)) = (( chi ( [:A, B:], [:X, Y:])) . (x,y)) by A5;

        end;

      end;

    end;

    registration

      let A,B be set;

      cluster ( chi (A,B)) -> nonnegative;

      coherence

      proof

        for x be object holds (( chi (A,B)) . x) >= 0

        proof

          let x be object;

          per cases ;

            suppose x in B & x in A;

            hence (( chi (A,B)) . x) >= 0 by FUNCT_3:def 3;

          end;

            suppose x in B & not x in A;

            hence (( chi (A,B)) . x) >= 0 by FUNCT_3:def 3;

          end;

            suppose not x in B;

            then not x in ( dom ( chi (A,B)));

            hence (( chi (A,B)) . x) >= 0 by FUNCT_1:def 2;

          end;

        end;

        hence ( chi (A,B)) is nonnegative by SUPINF_2: 51;

      end;

    end

    theorem :: MEASUR10:3

    for X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, m be induced_Measure of S, P, M be induced_sigma_Measure of S, m holds ( COM M) is complete by MEASURE3: 20;

    definition

      :: MEASUR10:def1

      func Family_of_Intervals -> semialgebra_of_sets of REAL equals the set of all I where I be Interval;

      correctness by SRINGS_3: 28;

    end

    theorem :: MEASUR10:4

    

     Th02: Family_of_halflines c= Family_of_Intervals

    proof

      now

        let A be object;

        assume A in Family_of_halflines ;

        then

        consider r be Element of REAL such that

         A1: A = ( halfline r) by PROB_1:def 11;

        A = ]. -infty , r.[ by A1, PROB_1:def 10;

        hence A in Family_of_Intervals by A1;

      end;

      hence thesis;

    end;

    

     Lm01: for I be Subset of REAL st I is open_interval holds I in Borel_Sets

    proof

      let I be Subset of REAL ;

      assume I is open_interval;

      then

      consider a,b be R_eal such that

       A1: I = ].a, b.[ by MEASURE5:def 2;

      

       A2: Family_of_halflines c= Borel_Sets by PROB_1:def 9, PROB_1:def 12;

      per cases by XXREAL_0: 14;

        suppose a = +infty ;

        then I = {} by A1, XXREAL_0: 3, XXREAL_1: 28;

        hence I in Borel_Sets by MEASURE1: 7;

      end;

        suppose

         A3: a = -infty ;

        per cases by XXREAL_0: 14;

          suppose b = +infty ;

          hence I in Borel_Sets by A1, A3, XXREAL_1: 224, FINANCE2: 11;

        end;

          suppose b = -infty ;

          then I = {} by A1, A3, XXREAL_1: 20;

          hence I in Borel_Sets by MEASURE1: 7;

        end;

          suppose

           A4: b in REAL ;

          I = ( halfline b) by A1, A3, PROB_1:def 10;

          then I in Family_of_halflines by A4, PROB_1:def 11;

          hence I in Borel_Sets by A2;

        end;

      end;

        suppose

         A8: a in REAL ;

        then

        reconsider a1 = a as Real;

        per cases by XXREAL_0: 14;

          suppose

           A6: b = +infty ;

          then [.a1, b.[ is Element of Borel_Sets by FINANCE1: 3;

          then

           A7: {a} in Borel_Sets & [.a, b.[ in Borel_Sets by FINANCE2: 5;

          I = ( [.a, b.[ \ {a}) by A1, A6, A8, XXREAL_0: 9, XXREAL_1: 136;

          hence I in Borel_Sets by A7, MEASURE1: 6;

        end;

          suppose b = -infty ;

          then I = {} by A1, XXREAL_1: 210;

          hence I in Borel_Sets by MEASURE1: 7;

        end;

          suppose b in REAL ;

          then

           A9: ].a, b.] is Element of Borel_Sets & {b} is Element of Borel_Sets by A8, FINANCE2: 5, FINANCE2: 6;

          per cases ;

            suppose a < b;

            then I = ( ].a, b.] \ {b}) by A1, XXREAL_1: 137;

            hence I in Borel_Sets by A9, MEASURE1: 6;

          end;

            suppose a >= b;

            then I = {} by A1, XXREAL_1: 28;

            hence I in Borel_Sets by MEASURE1: 7;

          end;

        end;

      end;

    end;

    

     Lm02: for I be Subset of REAL st I is closed_interval holds I in Borel_Sets

    proof

      let I be Subset of REAL ;

      assume I is closed_interval;

      then

      consider a,b be Real such that

       A1: I = [.a, b.] by MEASURE5:def 3;

      

       A2: ].a, b.] is Element of Borel_Sets & {a} is Element of Borel_Sets by FINANCE2: 5, FINANCE2: 6;

      per cases ;

        suppose a <= b;

        then I = ( ].a, b.] \/ {a}) by A1, XXREAL_1: 130;

        hence I in Borel_Sets by A2, MEASURE1: 11;

      end;

        suppose a > b;

        then I = {} by A1, XXREAL_1: 29;

        hence I in Borel_Sets by MEASURE1: 7;

      end;

    end;

    

     Lm03: for I be Subset of REAL st I is right_open_interval holds I in Borel_Sets

    proof

      let I be Subset of REAL ;

      assume I is right_open_interval;

      then

      consider a be Real, b be R_eal such that

       A1: I = [.a, b.[ by MEASURE5:def 4;

      per cases by XXREAL_0: 14;

        suppose b = +infty ;

        then I is Element of Borel_Sets by A1, FINANCE1: 3;

        hence I in Borel_Sets ;

      end;

        suppose b = -infty ;

        then I = {} by A1, XXREAL_0: 5, XXREAL_1: 27;

        hence I in Borel_Sets by MEASURE1: 7;

      end;

        suppose b in REAL ;

        then I is Element of Borel_Sets by A1, FINANCE1: 4;

        hence I in Borel_Sets ;

      end;

    end;

    

     Lm04: for I be Subset of REAL st I is left_open_interval holds I in Borel_Sets

    proof

      let I be Subset of REAL ;

      assume I is left_open_interval;

      then

      consider a be R_eal, b be Real such that

       A1: I = ].a, b.] by MEASURE5:def 5;

      per cases by XXREAL_0: 14;

        suppose a = +infty ;

        then I = {} by A1, XXREAL_0: 3, XXREAL_1: 26;

        hence I in Borel_Sets by MEASURE1: 7;

      end;

        suppose

         A2: a = -infty ;

        then

         A3: a < b by XREAL_0:def 1, XXREAL_0: 12;

         ].a, b.[ is Element of Borel_Sets by A2, FINANCE1: 3;

        then ].a, b.[ in Borel_Sets & {b} in Borel_Sets by FINANCE2: 5;

        then ( ].a, b.[ \/ {b}) in Borel_Sets by MEASURE1: 11;

        hence I in Borel_Sets by A1, A3, XXREAL_1: 132;

      end;

        suppose a in REAL ;

        then I is Element of Borel_Sets by A1, FINANCE2: 6;

        hence I in Borel_Sets ;

      end;

    end;

    theorem :: MEASUR10:5

    

     Th03: for I be Subset of REAL st I is Interval holds I in Borel_Sets

    proof

      let I be Subset of REAL ;

      assume I is Interval;

      then I is open_interval or I is closed_interval or I is right_open_interval or I is left_open_interval by MEASURE5: 1;

      hence thesis by Lm01, Lm02, Lm03, Lm04;

    end;

    theorem :: MEASUR10:6

    ( sigma Family_of_Intervals ) = Borel_Sets & ( sigma ( Field_generated_by Family_of_Intervals )) = Borel_Sets

    proof

       Family_of_Intervals c= ( sigma Family_of_Intervals ) by PROB_1:def 9;

      then

       A1: Family_of_halflines c= ( sigma Family_of_Intervals ) by Th02;

      now

        let x be object;

        assume x in Family_of_Intervals ;

        then ex I be Interval st x = I;

        hence x in Borel_Sets by Th03;

      end;

      then Family_of_Intervals c= Borel_Sets ;

      hence ( sigma Family_of_Intervals ) = Borel_Sets by A1, PROB_1:def 9, PROB_1:def 12;

      hence thesis by SRINGS_3: 23;

    end;

    begin

    theorem :: MEASUR10:7

    

     Th05: for X1,X2 be set, S1 be non empty Subset-Family of X1, S2 be non empty Subset-Family of X2 holds the set of all [:a, b:] where a be Element of S1, b be Element of S2 is non empty Subset-Family of [:X1, X2:]

    proof

      let X1,X2 be set;

      let S1 be non empty Subset-Family of X1;

      let S2 be non empty Subset-Family of X2;

      set L = the set of all [:a, b:] where a be Element of S1, b be Element of S2;

      

       A1: L = { s where s be Subset of [:X1, X2:] : ex x1,x2 be set st x1 in S1 & x2 in S2 & s = [:x1, x2:] } by SRINGS_2: 2;

      consider a be object such that

       A2: a in S1 by XBOOLE_0:def 1;

      consider b be object such that

       A3: b in S2 by XBOOLE_0:def 1;

      reconsider a as Element of S1 by A2;

      reconsider b as Element of S2 by A3;

      

       A4: [:a, b:] in L;

      now

        let z be object;

        assume z in L;

        then ex s be Subset of [:X1, X2:] st z = s & ex x1,x2 be set st x1 in S1 & x2 in S2 & s = [:x1, x2:] by A1;

        hence z in ( bool [:X1, X2:]);

      end;

      then L c= ( bool [:X1, X2:]);

      hence thesis by A4;

    end;

    theorem :: MEASUR10:8

    for X,Y be set, M be with_empty_element Subset-Family of X, N be with_empty_element Subset-Family of Y holds the set of all [:A, B:] where A be Element of M, B be Element of N is with_empty_element Subset-Family of [:X, Y:]

    proof

      let X,Y be set;

      let M be with_empty_element Subset-Family of X, N be with_empty_element Subset-Family of Y;

      set L = the set of all [:A, B:] where A be Element of M, B be Element of N;

      reconsider E1 = {} as Element of M by SETFAM_1:def 8;

      reconsider E2 = {} as Element of N by SETFAM_1:def 8;

       {} = [:E1, E2:] by ZFMISC_1: 90;

      then {} in L;

      hence thesis by Th05;

    end;

    theorem :: MEASUR10:9

    

     Th07: for X be set, F1,F2 be disjoint_valued FinSequence of X st ( union ( rng F1)) misses ( union ( rng F2)) holds (F1 ^ F2) is disjoint_valued FinSequence of X

    proof

      let X be set;

      let F1,F2 be disjoint_valued FinSequence of X;

      assume

       A1: ( union ( rng F1)) misses ( union ( rng F2));

      now

        let x,y be object;

        assume

         A2: x <> y;

        per cases ;

          suppose

           A3: x in ( dom (F1 ^ F2)) & y in ( dom (F1 ^ F2));

          then

          reconsider i = x, j = y as Nat;

          per cases ;

            suppose

             A4: i in ( dom F1);

            then

             A5: ((F1 ^ F2) . x) = (F1 . i) by FINSEQ_1:def 7;

            per cases ;

              suppose j in ( dom F1);

              then ((F1 ^ F2) . y) = (F1 . j) by FINSEQ_1:def 7;

              hence ((F1 ^ F2) . x) misses ((F1 ^ F2) . y) by A2, A5, PROB_2:def 2;

            end;

              suppose not j in ( dom F1);

              then

              consider j1 be Nat such that

               A6: j1 in ( dom F2) & j = (( len F1) + j1) by A3, FINSEQ_1: 25;

              ((F1 ^ F2) . y) = (F2 . j1) by A6, FINSEQ_1:def 7;

              then ((F1 ^ F2) . x) c= ( union ( rng F1)) & ((F1 ^ F2) . y) c= ( union ( rng F2)) by A4, A5, A6, FUNCT_1: 3, ZFMISC_1: 74;

              hence ((F1 ^ F2) . x) misses ((F1 ^ F2) . y) by A1, XBOOLE_1: 64;

            end;

          end;

            suppose not i in ( dom F1);

            then

            consider i1 be Nat such that

             A7: i1 in ( dom F2) & i = (( len F1) + i1) by A3, FINSEQ_1: 25;

            

             A8: ((F1 ^ F2) . x) = (F2 . i1) by A7, FINSEQ_1:def 7;

            per cases ;

              suppose

               A9: j in ( dom F1);

              then ((F1 ^ F2) . y) = (F1 . j) by FINSEQ_1:def 7;

              then ((F1 ^ F2) . x) c= ( union ( rng F2)) & ((F1 ^ F2) . y) c= ( union ( rng F1)) by A7, A8, A9, FUNCT_1: 3, ZFMISC_1: 74;

              hence ((F1 ^ F2) . x) misses ((F1 ^ F2) . y) by A1, XBOOLE_1: 64;

            end;

              suppose not j in ( dom F1);

              then

              consider j1 be Nat such that

               A10: j1 in ( dom F2) & j = (( len F1) + j1) by A3, FINSEQ_1: 25;

              ((F1 ^ F2) . y) = (F2 . j1) by A10, FINSEQ_1:def 7;

              hence ((F1 ^ F2) . x) misses ((F1 ^ F2) . y) by A2, A7, A10, A8, PROB_2:def 2;

            end;

          end;

        end;

          suppose not x in ( dom (F1 ^ F2)) or not y in ( dom (F1 ^ F2));

          then ((F1 ^ F2) . x) = {} or ((F1 ^ F2) . y) = {} by FUNCT_1:def 2;

          hence ((F1 ^ F2) . x) misses ((F1 ^ F2) . y);

        end;

      end;

      hence thesis by PROB_2:def 2;

    end;

    theorem :: MEASUR10:10

    

     Th08: for X1,X2 be set, S1 be Semiring of X1, S2 be Semiring of X2 holds the set of all [:A, B:] where A be Element of S1, B be Element of S2 is Semiring of [:X1, X2:]

    proof

      let X1,X2 be set, S1 be Semiring of X1, S2 be Semiring of X2;

      

       A1: S1 is semiring_of_sets of X1 by SRINGS_3: 9;

      S2 is diff-c=-finite-partition-closed by SRINGS_3: 9;

      then the set of all [:A, B:] where A be Element of S1, B be Element of S2 is cap-closed semiring_of_sets of [:X1, X2:] by A1, SRINGS_4: 36;

      hence thesis by SRINGS_3: 10;

    end;

    theorem :: MEASUR10:11

    

     Th09: for X1,X2 be set, S1 be semialgebra_of_sets of X1, S2 be semialgebra_of_sets of X2 holds the set of all [:A, B:] where A be Element of S1, B be Element of S2 is semialgebra_of_sets of [:X1, X2:]

    proof

      let X1,X2 be set, S1 be semialgebra_of_sets of X1, S2 be semialgebra_of_sets of X2;

      set S = the set of all [:A, B:] where A be Element of S1, B be Element of S2;

      

       A1: S is Semiring of [:X1, X2:] by Th08;

      X1 in S1 & X2 in S2 by SRINGS_3:def 6;

      then [:X1, X2:] in S;

      hence thesis by A1, SRINGS_3:def 6;

    end;

    theorem :: MEASUR10:12

    for X1,X2 be set, F1 be Field_Subset of X1, F2 be Field_Subset of X2 holds the set of all [:A, B:] where A be Element of F1, B be Element of F2 is semialgebra_of_sets of [:X1, X2:]

    proof

      let X1,X2 be set, F1 be Field_Subset of X1, F2 be Field_Subset of X2;

      set S = the set of all [:A, B:] where A be Element of F1, B be Element of F2;

      F1 is semialgebra_of_sets of X1 & F2 is semialgebra_of_sets of X2 by SRINGS_3: 20;

      hence thesis by Th09;

    end;

    definition

      let n be non zero Nat, X be non-emptyn -element FinSequence;

      :: MEASUR10:def2

      mode SemialgebraFamily of X -> n -element FinSequence means

      : Def2: for i be Nat st i in ( Seg n) holds (it . i) is semialgebra_of_sets of (X . i);

      existence

      proof

        deffunc F( set) = ( bool (X . $1));

        consider p be FinSequence such that

         A1: ( len p) = n and

         A2: for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_1:sch 2;

        reconsider p as n -element FinSequence by A1, CARD_1:def 7;

        take p;

        hereby

          let i be Nat;

          assume

           A3: i in ( Seg n);

          reconsider Xi = (X . i) as set;

          reconsider BXi = ( bool Xi) as Subset-Family of Xi;

          

           A4: BXi is cap-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover with_empty_element Subset-Family of Xi;

          

           A5: i in ( dom p) by A3, A1, FINSEQ_1:def 3;

          then

           A6: (p . i) is with_empty_element semi-diff-closed cap-closed Subset-Family of (X . i) by A2, A4;

          (X . i) in ( bool (X . i)) by ZFMISC_1:def 1;

          then (X . i) in (p . i) by A2, A5;

          hence (p . i) is semialgebra_of_sets of (X . i) by A6, SRINGS_3:def 6;

        end;

      end;

    end

    

     Lm05: for n be non zero Nat, X be non-emptyn -element FinSequence, S be SemialgebraFamily of X holds S is cap-closed-yielding SemiringFamily of X

    proof

      let n be non zero Nat, X be non-emptyn -element FinSequence, S be SemialgebraFamily of X;

       A1:

      now

        let i be Nat;

        assume i in ( Seg n);

        then (S . i) is semialgebra_of_sets of (X . i) by Def2;

        hence (S . i) is semiring_of_sets of (X . i) by SRINGS_3: 9;

      end;

      for i be Nat st i in ( Seg n) holds (S . i) is cap-closed by Def2;

      hence thesis by A1, SRINGS_4:def 3, SRINGS_4:def 5;

    end;

    definition

      let n be non zero Nat, X be non-emptyn -element FinSequence;

      :: original: SemialgebraFamily

      redefine

      mode SemialgebraFamily of X -> cap-closed-yielding SemiringFamily of X ;

      correctness by Lm05;

    end

    theorem :: MEASUR10:13

    

     Th11: for n be non zero Nat, X be non-emptyn -element FinSequence, S be SemialgebraFamily of X holds for i be Nat st i in ( Seg n) holds (X . i) in (S . i)

    proof

      let n be non zero Nat, X be non-emptyn -element FinSequence, S be SemialgebraFamily of X;

      hereby

        let i be Nat;

        assume i in ( Seg n);

        then (S . i) is semialgebra_of_sets of (X . i) by Def2;

        hence (X . i) in (S . i) by SRINGS_3:def 6;

      end;

    end;

    theorem :: MEASUR10:14

    

     Th12: for X be non-empty1 -element FinSequence, S be SemialgebraFamily of X holds the set of all ( product <*s*>) where s be Element of (S . 1) is semialgebra_of_sets of the set of all <*x*> where x be Element of (X . 1)

    proof

      let X be non-empty1 -element FinSequence, S be SemialgebraFamily of X;

      set S1 = the set of all ( product <*s*>) where s be Element of (S . 1);

      set X1 = the set of all <*x*> where x be Element of (X . 1);

      

       A1: 1 in ( Seg 1);

      then (X . 1) in (S . 1) by Th11;

      then

       A3: ( product <*(X . 1)*>) in S1;

      S1 is cap-closed semiring_of_sets of X1 by SRINGS_4: 34;

      then

       A5: S1 is with_empty_element semi-diff-closed cap-closed Subset-Family of X1 by SRINGS_3: 10;

      1 in ( dom X) by A1, FINSEQ_1: 89;

      then ( product <*(X . 1)*>) = the set of all <*y*> where y be Element of (X . 1) by SRINGS_4: 24;

      hence thesis by A3, A5, SRINGS_3:def 6;

    end;

    theorem :: MEASUR10:15

    

     Th13: for X be non-empty1 -element FinSequence, S be SemialgebraFamily of X holds ( SemiringProduct S) is semialgebra_of_sets of ( product X)

    proof

      let X be non-empty1 -element FinSequence, S be SemialgebraFamily of X;

      set S1 = the set of all ( product <*s*>) where s be Element of (S . 1);

      set X1 = the set of all <*x*> where x be Element of (X . 1);

      S1 = ( SemiringProduct S) & X1 = ( product X) by SRINGS_4: 23, SRINGS_4: 25;

      hence thesis by Th12;

    end;

    theorem :: MEASUR10:16

    

     Th14: for X1,X2 be set, S1 be semialgebra_of_sets of X1, S2 be semialgebra_of_sets of X2 holds the set of all [:s1, s2:] where s1 be Element of S1, s2 be Element of S2 is semialgebra_of_sets of [:X1, X2:]

    proof

      let X1,X2 be set, S1 be semialgebra_of_sets of X1, S2 be semialgebra_of_sets of X2;

      set S = the set of all [:s1, s2:] where s1 be Element of S1, s2 be Element of S2;

      S1 is cap-closed semiring_of_sets of X1 & S2 is cap-closed semiring_of_sets of X2 by SRINGS_3: 9;

      then S is cap-closed semiring_of_sets of [:X1, X2:] by SRINGS_4: 36;

      then

       A1: S is with_empty_element semi-diff-closed cap-closed Subset-Family of [:X1, X2:] by SRINGS_3: 10;

      X1 in S1 & X2 in S2 by SRINGS_3:def 6;

      then [:X1, X2:] in S;

      hence thesis by A1, SRINGS_3:def 6;

    end;

    theorem :: MEASUR10:17

    

     Th15: for n be non zero Nat, X be non-emptyn -element FinSequence, S be SemialgebraFamily of X holds ( SemiringProduct S) is semialgebra_of_sets of ( product X)

    proof

      let n be non zero Nat, X be non-emptyn -element FinSequence, S be SemialgebraFamily of X;

      defpred P[ non zero Nat] means for X be non-empty$1 -element FinSequence, S be SemialgebraFamily of X holds ( SemiringProduct S) is semialgebra_of_sets of ( product X);

      

       A1: P[1] by Th13;

       A2:

      now

        let k be non zero Nat;

        assume P[k];

        now

          let Xn1 be non-empty(k + 1) -element FinSequence, Sn1 be SemialgebraFamily of Xn1;

          

           A3: ( SemiringProduct Sn1) is cap-closed semiring_of_sets of ( product Xn1) by SRINGS_4: 38;

          then

           A4: ( SemiringProduct Sn1) is semi-diff-closed by SRINGS_3: 10;

          

           A6: ( dom Xn1) = ( dom Sn1) by SRINGS_4: 18;

          now

            let x be object;

            assume x in ( dom Sn1);

            then x in ( Seg (k + 1)) by FINSEQ_1: 89;

            hence (Xn1 . x) in (Sn1 . x) by Th11;

          end;

          then Xn1 in ( product Sn1) by A6, CARD_3: 9;

          then ( product Xn1) in ( SemiringProduct Sn1) by SRINGS_4:def 4;

          hence ( SemiringProduct Sn1) is semialgebra_of_sets of ( product Xn1) by A3, A4, SRINGS_3:def 6;

        end;

        hence P[(k + 1)];

      end;

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

      hence thesis;

    end;

    theorem :: MEASUR10:18

    for n be non zero Nat, Xn be non-emptyn -element FinSequence, X1 be non-empty1 -element FinSequence, Sn be SemialgebraFamily of Xn, S1 be SemialgebraFamily of X1 holds ( SemiringProduct (Sn ^ S1)) is semialgebra_of_sets of ( product (Xn ^ X1))

    proof

      let n be non zero Nat, Xn be non-emptyn -element FinSequence, X1 be non-empty1 -element FinSequence, Sn be SemialgebraFamily of Xn, S1 be SemialgebraFamily of X1;

      

       A1: ( SemiringProduct Sn) is semialgebra_of_sets of ( product Xn) & ( SemiringProduct S1) is semialgebra_of_sets of ( product X1) by Th15;

      reconsider S12 = the set of all [:s1, s2:] where s1 be Element of ( SemiringProduct Sn), s2 be Element of ( SemiringProduct S1) as semialgebra_of_sets of [:( product Xn), ( product X1):] by A1, Th14;

      ( SemiringProduct Sn) is cap-closed semiring_of_sets of ( product Xn) & ( SemiringProduct S1) is cap-closed semiring_of_sets of ( product X1) by SRINGS_4: 38;

      then

       A5: ( SemiringProduct (Sn ^ S1)) is cap-closed semiring_of_sets of ( product (Xn ^ X1)) by SRINGS_4: 37;

      then

       A6: ( SemiringProduct (Sn ^ S1)) is semi-diff-closed by SRINGS_3: 10;

      

       A11: ( dom Xn) = ( dom Sn) & ( dom X1) = ( dom S1) by SRINGS_4: 18;

      then

       A8: ( len Xn) = ( len Sn) & ( len X1) = ( len S1) by FINSEQ_3: 29;

      ( len (Xn ^ X1)) = (( len Xn) + ( len X1)) & ( len (Sn ^ S1)) = (( len Sn) + ( len S1)) by FINSEQ_1: 22;

      then

       A7: ( dom (Xn ^ X1)) = ( dom (Sn ^ S1)) by A8, FINSEQ_3: 29;

      now

        let x be object;

        assume

         A9: x in ( dom (Sn ^ S1));

        per cases by A9, FINSEQ_1: 25;

          suppose

           A10: x in ( dom Sn);

          then x in ( Seg n) by FINSEQ_1: 89;

          then (Xn . x) in (Sn . x) by Th11;

          then ((Xn ^ X1) . x) in (Sn . x) by A10, A11, FINSEQ_1:def 7;

          hence ((Xn ^ X1) . x) in ((Sn ^ S1) . x) by A10, FINSEQ_1:def 7;

        end;

          suppose ex k be Nat st k in ( dom S1) & x = (( len Sn) + k);

          then

          consider k be Nat such that

           A12: k in ( dom S1) & x = (( len Sn) + k);

          k in ( Seg 1) by A12, FINSEQ_1: 89;

          then (X1 . k) in (S1 . k) by Th11;

          then ((Xn ^ X1) . x) in (S1 . k) by A12, A11, A8, FINSEQ_1:def 7;

          hence ((Xn ^ X1) . x) in ((Sn ^ S1) . x) by A12, FINSEQ_1:def 7;

        end;

      end;

      then (Xn ^ X1) in ( product (Sn ^ S1)) by A7, CARD_3: 9;

      then ( product (Xn ^ X1)) in ( SemiringProduct (Sn ^ S1)) by SRINGS_4:def 4;

      hence thesis by A5, A6, SRINGS_3:def 6;

    end;

    definition

      let n be non zero Nat, X be non-emptyn -element FinSequence;

      :: MEASUR10:def3

      mode FieldFamily of X -> n -element FinSequence means

      : Def3: for i be Nat st i in ( Seg n) holds (it . i) is Field_Subset of (X . i);

      existence

      proof

        deffunc F( set) = ( bool (X . $1));

        consider p be FinSequence such that

         A1: ( len p) = n and

         A2: for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_1:sch 2;

        reconsider p as n -element FinSequence by A1, CARD_1:def 7;

        take p;

        hereby

          let i be Nat;

          assume i in ( Seg n);

          then i in ( dom p) by A1, FINSEQ_1:def 3;

          then (p . i) = ( bool (X . i)) by A2;

          hence (p . i) is Field_Subset of (X . i);

        end;

      end;

    end

    

     Lm06: for n be non zero Nat, X be non-emptyn -element FinSequence, S be FieldFamily of X holds S is SemialgebraFamily of X

    proof

      let n be non zero Nat, X be non-emptyn -element FinSequence, S be FieldFamily of X;

      for i be Nat st i in ( Seg n) holds (S . i) is semialgebra_of_sets of (X . i)

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (S . i) is Field_Subset of (X . i) by Def3;

        hence thesis by SRINGS_3: 20;

      end;

      hence thesis by Def2;

    end;

    definition

      let n be non zero Nat, X be non-emptyn -element FinSequence;

      :: original: FieldFamily

      redefine

      mode FieldFamily of X -> SemialgebraFamily of X ;

      correctness by Lm06;

    end

    theorem :: MEASUR10:19

    

     Th17: for X be non-empty1 -element FinSequence, S be FieldFamily of X holds the set of all ( product <*s*>) where s be Element of (S . 1) is Field_Subset of the set of all <*x*> where x be Element of (X . 1)

    proof

      let X be non-empty1 -element FinSequence, S be FieldFamily of X;

      set S1 = the set of all ( product <*s*>) where s be Element of (S . 1);

      set X1 = the set of all <*x*> where x be Element of (X . 1);

      ( dom X) = ( Seg 1) by FINSEQ_1: 89;

      then

       A1: ( len X) = 1 by FINSEQ_1:def 3;

      

       A2: 1 in ( Seg 1);

      then 1 in ( dom X) by FINSEQ_1: 89;

      then

       A4: X1 = ( product <*(X . 1)*>) by SRINGS_4: 24;

      

       A5: X = <*(X . 1)*> by A1, FINSEQ_1: 40;

      reconsider F = (S . 1) as Field_Subset of (X . 1) by A2, Def3;

      F is non empty;

      then

      consider s be object such that

       A7: s in F;

      reconsider s as Element of (S . 1) by A7;

      S1 = ( SemiringProduct S) by SRINGS_4: 25;

      then

      reconsider S1 as Subset-Family of ( product X) by SRINGS_4: 22;

      now

        let A be set;

        assume A in S1;

        then

        consider s be Element of (S . 1) such that

         A8: A = ( product <*s*>);

        ((X . 1) \ s) in F by MEASURE1:def 1;

        then ( product <*((X . 1) \ s)*>) in S1;

        hence (( product X) \ A) in S1 by A5, A8, SRINGS_4: 27;

      end;

      hence thesis by A4, A5, Th12, MEASURE1:def 1;

    end;

    theorem :: MEASUR10:20

    for X be non-empty1 -element FinSequence, S be FieldFamily of X holds ( SemiringProduct S) is Field_Subset of ( product X)

    proof

      let X be non-empty1 -element FinSequence, S be SemialgebraFamily of X;

      set S1 = the set of all ( product <*s*>) where s be Element of (S . 1);

      set X1 = the set of all <*x*> where x be Element of (X . 1);

      S1 = ( SemiringProduct S) & X1 = ( product X) by SRINGS_4: 23, SRINGS_4: 25;

      hence thesis by Th17;

    end;

    definition

      let n be non zero Nat, X be non-emptyn -element FinSequence, S be FieldFamily of X;

      :: MEASUR10:def4

      mode MeasureFamily of S -> n -element FinSequence means for i be Nat st i in ( Seg n) holds ex F be Field_Subset of (X . i) st F = (S . i) & (it . i) is Measure of F;

      existence

      proof

        defpred P[ Nat, object] means ex F be Field_Subset of (X . $1) st F = (S . $1) & $2 is Measure of F;

         A0:

        now

          let i be Nat;

          assume i in ( Seg n);

          then

          reconsider F = (S . i) as Field_Subset of (X . i) by Def3;

          reconsider M = (F --> 0. ) as Function of F, ExtREAL ;

          

           A1: for A,B be Element of F st A misses B holds (M . (A \/ B)) = ((M . A) + (M . B))

          proof

            let A,B be Element of F;

            assume A misses B;

            

             A2: (M . A) = 0. & (M . B) = 0. by FUNCOP_1: 7;

            reconsider A, B as Element of (S . i);

             0. = ((M . A) + (M . B)) by A2;

            hence thesis by FUNCOP_1: 7;

          end;

          (for x be Element of (S . i) holds 0. <= (M . x)) & (M . {} ) = 0. by FUNCOP_1: 7, PROB_1: 4;

          then M is nonnegative additive zeroed Function of F, ExtREAL by A1, VALUED_0:def 19, MEASURE1:def 8, SUPINF_2: 39;

          hence ex M be object st P[i, M];

        end;

        consider M be FinSequence such that

         A4: ( dom M) = ( Seg n) & for i be Nat st i in ( Seg n) holds P[i, (M . i)] from FINSEQ_1:sch 1( A0);

        ( Seg ( len M)) = ( Seg n) by A4, FINSEQ_1:def 3;

        then

        reconsider M as n -element FinSequence by CARD_1:def 7, FINSEQ_1: 6;

        take M;

        thus thesis by A4;

      end;

    end

    begin

    definition

      let X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2;

      :: MEASUR10:def5

      func measurable_rectangles (S1,S2) -> semialgebra_of_sets of [:X1, X2:] equals the set of all [:A, B:] where A be Element of S1, B be Element of S2;

      correctness

      proof

        S1 is semialgebra_of_sets of X1 & S2 is semialgebra_of_sets of X2 by SRINGS_3: 20;

        hence thesis by Th09;

      end;

    end

    theorem :: MEASUR10:21

    for X be set, F be Field_Subset of X holds ex S be semialgebra_of_sets of X st F = S & F = ( Field_generated_by S)

    proof

      let X be set, F be Field_Subset of X;

      reconsider S = F as semialgebra_of_sets of X by SRINGS_3: 20;

      take S;

      now

        let x be object;

        assume x in ( Field_generated_by S);

        then

         A2: x in ( meet { Z where Z be Field_Subset of X : S c= Z }) by SRINGS_3:def 7;

        F in { Z where Z be Field_Subset of X : S c= Z };

        hence x in S by A2, SETFAM_1:def 1;

      end;

      then ( Field_generated_by S) c= S;

      hence thesis by SRINGS_3: 21;

    end;

    definition

      let X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2, m1 be Measure of S1, m2 be Measure of S2;

      :: MEASUR10:def6

      func product-pre-Measure (m1,m2) -> nonnegative zeroed Function of ( measurable_rectangles (S1,S2)), ExtREAL means

      : Def6: for C be Element of ( measurable_rectangles (S1,S2)) holds ex A be Element of S1, B be Element of S2 st C = [:A, B:] & (it . C) = ((m1 . A) * (m2 . B));

      existence

      proof

        defpred P[ Element of ( measurable_rectangles (S1,S2)), Element of ExtREAL ] means ex A be Element of S1, B be Element of S2 st $1 = [:A, B:] & $2 = ((m1 . A) * (m2 . B));

        

         A1: for C be Element of ( measurable_rectangles (S1,S2)) holds ex y be Element of ExtREAL st P[C, y]

        proof

          let C be Element of ( measurable_rectangles (S1,S2));

          C in the set of all [:A, B:] where A be Element of S1, B be Element of S2;

          then

          consider A be Element of S1, B be Element of S2 such that

           A2: C = [:A, B:];

          set y = ((m1 . A) * (m2 . B));

          take y;

          thus thesis by A2;

        end;

        consider IT be Function of ( measurable_rectangles (S1,S2)), ExtREAL such that

         A3: for C be Element of ( measurable_rectangles (S1,S2)) holds P[C, (IT . C)] from FUNCT_2:sch 3( A1);

         A6:

        now

          let x be object;

          assume x in ( dom IT);

          then

          reconsider C = x as Element of ( measurable_rectangles (S1,S2));

          consider A be Element of S1, B be Element of S2 such that

           A5: C = [:A, B:] & (IT . C) = ((m1 . A) * (m2 . B)) by A3;

           0 <= (m1 . A) & 0 <= (m2 . B) by SUPINF_2: 51;

          hence 0 <= (IT . x) by A5;

        end;

        reconsider Z = {} as Element of ( measurable_rectangles (S1,S2)) by SETFAM_1:def 8;

        consider A0 be Element of S1, B0 be Element of S2 such that

         A7: Z = [:A0, B0:] & (IT . Z) = ((m1 . A0) * (m2 . B0)) by A3;

        A0 = {} or B0 = {} by A7;

        then (m1 . A0) = 0 or (m2 . B0) = 0 by VALUED_0:def 19;

        then (IT . {} ) = 0 by A7;

        then

        reconsider IT as nonnegative zeroed Function of ( measurable_rectangles (S1,S2)), ExtREAL by A6, SUPINF_2: 52, VALUED_0:def 19;

        take IT;

        thus for C be Element of ( measurable_rectangles (S1,S2)) holds ex A be Element of S1, B be Element of S2 st C = [:A, B:] & (IT . C) = ((m1 . A) * (m2 . B)) by A3;

      end;

      uniqueness

      proof

        let F1,F2 be nonnegative zeroed Function of ( measurable_rectangles (S1,S2)), ExtREAL ;

        assume that

         A1: for C be Element of ( measurable_rectangles (S1,S2)) holds ex A be Element of S1, B be Element of S2 st C = [:A, B:] & (F1 . C) = ((m1 . A) * (m2 . B)) and

         A2: for C be Element of ( measurable_rectangles (S1,S2)) holds ex A be Element of S1, B be Element of S2 st C = [:A, B:] & (F2 . C) = ((m1 . A) * (m2 . B));

        now

          let C be Element of ( measurable_rectangles (S1,S2));

          consider A1 be Element of S1, B1 be Element of S2 such that

           A3: C = [:A1, B1:] & (F1 . C) = ((m1 . A1) * (m2 . B1)) by A1;

          consider A2 be Element of S1, B2 be Element of S2 such that

           A4: C = [:A2, B2:] & (F2 . C) = ((m1 . A2) * (m2 . B2)) by A2;

          per cases ;

            suppose

             A5: A1 = {} or B1 = {} ;

            then A2 = {} or B2 = {} by A3, A4;

            then ((m1 . A1) = 0 or (m2 . B1) = 0 ) & ((m1 . A2) = 0 or (m2 . B2) = 0 ) by A5, VALUED_0:def 19;

            hence (F1 . C) = (F2 . C) by A3, A4;

          end;

            suppose A1 <> {} & B1 <> {} ;

            then A1 = A2 & B1 = B2 by A3, A4, ZFMISC_1: 110;

            hence (F1 . C) = (F2 . C) by A3, A4;

          end;

        end;

        hence F1 = F2 by FUNCT_2:def 8;

      end;

    end

    theorem :: MEASUR10:22

    

     Th20: for X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2, m1 be Measure of S1, m2 be Measure of S2, A,B be set st A in S1 & B in S2 holds (( product-pre-Measure (m1,m2)) . [:A, B:]) = ((m1 . A) * (m2 . B))

    proof

      let X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2, m1 be Measure of S1, m2 be Measure of S2, A,B be set;

      assume A in S1 & B in S2;

      then [:A, B:] in ( measurable_rectangles (S1,S2));

      then

      consider A1 be Element of S1, B1 be Element of S2 such that

       A2: [:A, B:] = [:A1, B1:] & (( product-pre-Measure (m1,m2)) . [:A, B:]) = ((m1 . A1) * (m2 . B1)) by Def6;

      per cases ;

        suppose

         A3: A = {} or B = {} ;

        then [:A, B:] = {} by ZFMISC_1: 90;

        then

         A4: (( product-pre-Measure (m1,m2)) . [:A, B:]) = 0 by VALUED_0:def 19;

        (m1 . A) = 0 or (m2 . B) = 0 by A3, VALUED_0:def 19;

        hence thesis by A4;

      end;

        suppose A <> {} & B <> {} ;

        then A = A1 & B = B1 by A2, ZFMISC_1: 110;

        hence thesis by A2;

      end;

    end;

    theorem :: MEASUR10:23

    for X1,X2 be set, S1 be non empty Subset-Family of X1, S2 be non empty Subset-Family of X2, S be non empty Subset-Family of [:X1, X2:], H be FinSequence of S st S = the set of all [:A, B:] where A be Element of S1, B be Element of S2 holds ex F be FinSequence of S1, G be FinSequence of S2 st ( len H) = ( len F) & ( len H) = ( len G) & for k be Nat st k in ( dom H) & (H . k) <> {} holds (H . k) = [:(F . k), (G . k):]

    proof

      let X1,X2 be set, S1 be non empty Subset-Family of X1, S2 be non empty Subset-Family of X2, S be non empty Subset-Family of [:X1, X2:], H be FinSequence of S;

      assume

       AS: S = the set of all [:A, B:] where A be Element of S1, B be Element of S2;

      

       A1: for k be Nat st k in ( dom H) holds ex A be Element of S1, B be Element of S2 st (H . k) = [:A, B:]

      proof

        let k be Nat;

        assume

         A2: k in ( dom H);

        (H /. k) in S;

        then (H . k) in S by A2, PARTFUN1:def 6;

        hence thesis by AS;

      end;

      defpred P1[ Nat, set] means ex B be Element of S2 st (H . $1) = [:$2, B:];

      ( Seg ( len H)) = ( dom H) by FINSEQ_1:def 3;

      then

       A3: for k be Nat st k in ( Seg ( len H)) holds ex A be Element of S1 st P1[k, A] by A1;

      consider F be FinSequence of S1 such that

       A4: ( dom F) = ( Seg ( len H)) & for k be Nat st k in ( Seg ( len H)) holds P1[k, (F . k)] from FINSEQ_1:sch 5( A3);

      defpred P2[ Nat, set] means ex A be Element of S1 st (H . $1) = [:A, $2:];

      

       A5: for k be Nat st k in ( Seg ( len H)) holds ex B be Element of S2 st P2[k, B]

      proof

        let k be Nat;

        assume k in ( Seg ( len H));

        then k in ( dom H) by FINSEQ_1:def 3;

        then ex A be Element of S1, B be Element of S2 st (H . k) = [:A, B:] by A1;

        hence thesis;

      end;

      consider G be FinSequence of S2 such that

       A6: ( dom G) = ( Seg ( len H)) & for k be Nat st k in ( Seg ( len H)) holds P2[k, (G . k)] from FINSEQ_1:sch 5( A5);

      take F, G;

      thus ( len H) = ( len F) & ( len H) = ( len G) by A4, A6, FINSEQ_1:def 3;

      hereby

        let k be Nat;

        assume

         A8: k in ( dom H) & (H . k) <> {} ;

        then

         A9: k in ( Seg ( len H)) by FINSEQ_1:def 3;

        then

        consider B be Element of S2 such that

         A10: (H . k) = [:(F . k), B:] by A4;

        consider A be Element of S1 such that

         A11: (H . k) = [:A, (G . k):] by A9, A6;

        (F . k) <> {} & B <> {} by A8, A10;

        hence (H . k) = [:(F . k), (G . k):] by A10, A11, ZFMISC_1: 110;

      end;

    end;

    theorem :: MEASUR10:24

    for X be set, S be non empty semi-diff-closed cap-closed Subset-Family of X, E1,E2 be Element of S holds ex F1,F2,F3 be disjoint_valued FinSequence of S st ( union ( rng F1)) = (E1 \ E2) & ( union ( rng F2)) = (E2 \ E1) & ( union ( rng F3)) = (E1 /\ E2) & ((F1 ^ F2) ^ F3) is disjoint_valued FinSequence of S

    proof

      let X be set, S be non empty semi-diff-closed cap-closed Subset-Family of X, E1,E2 be Element of S;

      consider F1 be disjoint_valued FinSequence of S such that

       A2: (E1 \ E2) = ( Union F1) by SRINGS_3:def 1;

      consider F2 be disjoint_valued FinSequence of S such that

       A3: (E2 \ E1) = ( Union F2) by SRINGS_3:def 1;

      (E1 \ E2) misses (E2 \ E1) by XBOOLE_1: 82;

      then ( union ( rng F1)) misses ( Union F2) by A2, A3, CARD_3:def 4;

      then ( union ( rng F1)) misses ( union ( rng F2)) by CARD_3:def 4;

      then

      reconsider G = (F1 ^ F2) as disjoint_valued FinSequence of S by Th07;

      ( rng G) = (( rng F1) \/ ( rng F2)) by FINSEQ_1: 31;

      then

       A4: ( union ( rng G)) = (( union ( rng F1)) \/ ( union ( rng F2))) by ZFMISC_1: 78;

      ( Union F1) = ( union ( rng F1)) & ( Union F2) = ( union ( rng F2)) by CARD_3:def 4;

      then ( Union G) = ((E1 \ E2) \/ (E2 \ E1)) by A2, A3, A4, CARD_3:def 4;

      then

       A5: ( Union G) = (E1 \+\ E2) by XBOOLE_0:def 6;

      reconsider E = (E1 /\ E2) as Element of S by FINSUB_1:def 2;

      reconsider F3 = <*E*> as FinSequence of S;

      reconsider F3 as disjoint_valued FinSequence of S;

      take F1, F2, F3;

      reconsider F = (G ^ <*E*>) as FinSequence of S;

      thus ( union ( rng F1)) = (E1 \ E2) & ( union ( rng F2)) = (E2 \ E1) by A2, A3, CARD_3:def 4;

      ( rng F3) = {E} by FINSEQ_1: 38;

      hence ( union ( rng F3)) = (E1 /\ E2) by ZFMISC_1: 25;

      

       A6: ( Union G) misses E by A5, XBOOLE_1: 103;

      

       B1: ( len F) = (( len G) + 1) by FINSEQ_2: 16;

       A7:

      now

        let i,j be Nat;

        assume

         A8: i in ( dom G) & j = ( len F);

        then

         A9: (F . j) = E by B1, FINSEQ_1: 42;

        (F . i) = (G . i) by A8, FINSEQ_1:def 7;

        then (F . i) c= ( union ( rng G)) by A8, FUNCT_1: 3, ZFMISC_1: 74;

        then (F . i) c= ( Union G) by CARD_3:def 4;

        hence (F . i) misses (F . j) by A6, A9, XBOOLE_1: 63;

      end;

      now

        let x,y be object;

        assume

         A10: x <> y;

        per cases ;

          suppose

           A11: x in ( dom F) & y in ( dom F);

          then

          reconsider x1 = x, y1 = y as Nat;

          

           A12: 1 <= x1 & x1 <= ( len F) & 1 <= y1 & y1 <= ( len F) by A11, FINSEQ_3: 25;

          per cases ;

            suppose

             A13: x1 = ( len F);

            then y1 < ( len F) by A10, A12, XXREAL_0: 1;

            then y1 <= ( len G) by B1, NAT_1: 13;

            hence (F . x) misses (F . y) by A7, A13, A12, FINSEQ_3: 25;

          end;

            suppose

             A11: y1 = ( len F);

            then x1 < ( len F) by A10, A12, XXREAL_0: 1;

            then x1 <= ( len G) by B1, NAT_1: 13;

            hence (F . x) misses (F . y) by A7, A11, A12, FINSEQ_3: 25;

          end;

            suppose x1 <> ( len F) & y1 <> ( len F);

            then x1 < ( len F) & y1 < ( len F) by A12, XXREAL_0: 1;

            then x1 <= ( len G) & y1 <= ( len G) by B1, NAT_1: 13;

            then x1 in ( dom G) & y1 in ( dom G) by A12, FINSEQ_3: 25;

            then (F . x) = (G . x) & (F . y) = (G . y) by FINSEQ_1:def 7;

            hence (F . x) misses (F . y) by A10, PROB_2:def 2;

          end;

        end;

          suppose not x in ( dom F) or not y in ( dom F);

          then (F . x) = {} or (F . y) = {} by FUNCT_1:def 2;

          hence (F . x) misses (F . y);

        end;

      end;

      hence thesis by PROB_2:def 2;

    end;

    theorem :: MEASUR10:25

    for X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2, m1 be Measure of S1, m2 be Measure of S2, E1,E2 be Element of ( measurable_rectangles (S1,S2)) st E1 misses E2 & (E1 \/ E2) in ( measurable_rectangles (S1,S2)) holds (( product-pre-Measure (m1,m2)) . (E1 \/ E2)) = ((( product-pre-Measure (m1,m2)) . E1) + (( product-pre-Measure (m1,m2)) . E2))

    proof

      let X1,X2 be set, S1 be Field_Subset of X1, S2 be Field_Subset of X2, m1 be Measure of S1, m2 be Measure of S2, E1,E2 be Element of ( measurable_rectangles (S1,S2));

      assume that

       A1: E1 misses E2 and

       A2: (E1 \/ E2) in ( measurable_rectangles (S1,S2));

      set S = ( measurable_rectangles (S1,S2));

      set P = ( product-pre-Measure (m1,m2));

      reconsider E = (E1 \/ E2) as Element of S by A2;

      consider A be Element of S1, B be Element of S2 such that

       A3: E = [:A, B:] & (P . E) = ((m1 . A) * (m2 . B)) by Def6;

      consider A1 be Element of S1, B1 be Element of S2 such that

       A4: E1 = [:A1, B1:] & (P . E1) = ((m1 . A1) * (m2 . B1)) by Def6;

      consider A2 be Element of S1, B2 be Element of S2 such that

       A5: E2 = [:A2, B2:] & (P . E2) = ((m1 . A2) * (m2 . B2)) by Def6;

      per cases ;

        suppose E1 = {} or E2 = {} ;

        then ((P . E1) = 0 & (P . E) = (P . E2)) or ((P . E2) = 0 & (P . E) = (P . E1)) by VALUED_0:def 19;

        hence (P . (E1 \/ E2)) = ((P . E1) + (P . E2)) by XXREAL_3: 4;

      end;

        suppose E1 <> {} & E2 <> {} ;

        then

         A11: A <> {} & B <> {} & A1 <> {} & B1 <> {} & A2 <> {} & B2 <> {} by A3, A4, A5;

        per cases by A1, A4, A5, A3, A11, Th23;

          suppose

           A13: A1 misses A2 & A = (A1 \/ A2) & B = B1 & B = B2;

          then ( [:A1, B1:] \/ [:A2, B2:]) = [:(A1 \/ A2), B:] by ZFMISC_1: 97;

          then (P . (E1 \/ E2)) = ((m1 . (A1 \/ A2)) * (m2 . B)) by A4, A5, Th20;

          then

           A14: (P . (E1 \/ E2)) = (((m1 . A1) + (m1 . A2)) * (m2 . B)) by A13, MEASURE1:def 3;

          (m1 . A1) >= 0 & (m1 . A2) >= 0 by MEASURE1:def 2;

          hence (P . (E1 \/ E2)) = ((P . E1) + (P . E2)) by A4, A5, A13, A14, XXREAL_3: 96;

        end;

          suppose

           A15: B1 misses B2 & B = (B1 \/ B2) & A = A1 & A = A2;

          then ( [:A1, B1:] \/ [:A2, B2:]) = [:A, (B1 \/ B2):] by ZFMISC_1: 97;

          then (P . (E1 \/ E2)) = ((m1 . A) * (m2 . (B1 \/ B2))) by A4, A5, Th20;

          then

           A16: (P . (E1 \/ E2)) = ((m1 . A) * ((m2 . B1) + (m2 . B2))) by A15, MEASURE1:def 3;

          (m2 . B1) >= 0 & (m2 . B2) >= 0 by MEASURE1:def 2;

          hence (P . (E1 \/ E2)) = ((P . E1) + (P . E2)) by A4, A5, A15, A16, XXREAL_3: 96;

        end;

      end;

    end;

    theorem :: MEASUR10:26

    

     Th25: for X be non empty set, S be non empty Subset-Family of X, f be Function of NAT , S, F be Functional_Sequence of X, ExtREAL st f is disjoint_valued & (for n be Nat holds (F . n) = ( chi ((f . n),X))) holds (for x be object st x in X holds (( chi (( Union f),X)) . x) = (( lim ( Partial_Sums F)) . x))

    proof

      let X be non empty set, S be non empty Subset-Family of X, f be Function of NAT , S, F be Functional_Sequence of X, ExtREAL ;

      assume

       A0: f is disjoint_valued;

      assume

       A1: for n be Nat holds (F . n) = ( chi ((f . n),X));

      let x be object;

      assume

       A2: x in X;

      then

      reconsider x1 = x as Element of X;

       A3:

      now

        let n,m be Nat;

        assume n <> m;

        hereby

          let x be set;

          assume x in (( dom (F . n)) /\ ( dom (F . m)));

          then

           A5: x in ( dom (F . n)) & x in ( dom (F . m)) by XBOOLE_0:def 4;

          (F . n) = ( chi ((f . n),X)) & (F . m) = ( chi ((f . m),X)) by A1;

          then ( rng (F . n)) c= { 0 , 1} & ( rng (F . m)) c= { 0 , 1} by FUNCT_3: 39;

          then not +infty in ( rng (F . n)) & not -infty in ( rng (F . m));

          hence ((F . n) . x) <> +infty or ((F . m) . x) <> -infty by A5, FUNCT_1: 3;

        end;

      end;

      now

        let n,m be Nat;

        (F . n) = ( chi ((f . n),X)) & (F . m) = ( chi ((f . m),X)) by A1;

        then ( dom (F . n)) = X & ( dom (F . m)) = X by FUNCT_3:def 3;

        hence ( dom (F . n)) = ( dom (F . m));

      end;

      then

       A9: F is with_the_same_dom by MESFUNC8:def 2;

      (F . 0 ) = ( chi ((f . 0 ),X)) by A1;

      then

       A20: ( dom (F . 0 )) = X by FUNCT_3:def 3;

      then ( dom (( Partial_Sums F) . 0 )) = X by MESFUNC9:def 4;

      then x in ( dom ( lim ( Partial_Sums F))) by A2, MESFUNC8:def 9;

      then

       A14: (( lim ( Partial_Sums F)) . x) = ( lim (( Partial_Sums F) # x1)) by MESFUNC8:def 9;

      per cases ;

        suppose

         A10: x in ( Union f);

        then x in ( union ( rng f)) by CARD_3:def 4;

        then

        consider V be set such that

         A11: x in V & V in ( rng f) by TARSKI:def 4;

        consider n be Element of NAT such that

         A12: V = (f . n) by A11, FUNCT_2: 113;

        

         A15: for m be Nat st m <> n holds ((F . m) . x1) = 0

        proof

          let m be Nat;

          assume m <> n;

          then not x in (f . m) by A0, PROB_2:def 2, A11, A12, XBOOLE_0: 3;

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

          hence ((F . m) . x1) = 0 by A1;

        end;

        defpred P1[ Nat] means $1 < n implies ((( Partial_Sums F) # x1) . $1) = 0 ;

        now

          assume

           A16: 0 < n;

          ((( Partial_Sums F) # x1) . 0 ) = ((( Partial_Sums F) . 0 ) . x1) by MESFUNC5:def 13

          .= ((F . 0 ) . x1) by MESFUNC9:def 4;

          hence ((( Partial_Sums F) # x1) . 0 ) = 0 by A15, A16;

        end;

        then

         A17: P1[ 0 ];

        

         A18: for k be Nat st P1[k] holds P1[(k + 1)]

        proof

          let k be Nat;

          assume

           A19: P1[k];

          assume

           A21: (k + 1) < n;

          then

           A22: (( Partial_Sums (F # x1)) . k) = 0 by A9, A19, A20, A3, MESFUNC9:def 5, MESFUNC9: 32, NAT_1: 13;

          ((( Partial_Sums F) # x1) . (k + 1)) = (( Partial_Sums (F # x1)) . (k + 1)) by A3, A9, A20, MESFUNC9:def 5, MESFUNC9: 32

          .= ((( Partial_Sums (F # x1)) . k) + ((F # x1) . (k + 1))) by MESFUNC9:def 1

          .= ((F # x1) . (k + 1)) by A22, XXREAL_3: 4

          .= ((F . (k + 1)) . x1) by MESFUNC5:def 13;

          hence ((( Partial_Sums F) # x1) . (k + 1)) = 0 by A15, A21;

        end;

        

         A23: for k be Nat holds P1[k] from NAT_1:sch 2( A17, A18);

        defpred P2[ Nat] means $1 >= n implies ((( Partial_Sums F) # x1) . $1) = 1;

        now

          assume 0 >= n;

          then

           A24: n = 0 ;

          

           A25: ((( Partial_Sums F) # x1) . 0 ) = ((( Partial_Sums F) . 0 ) . x1) by MESFUNC5:def 13

          .= ((F . 0 ) . x1) by MESFUNC9:def 4;

          (F . 0 ) = ( chi ((f . n),X)) by A24, A1;

          hence ((( Partial_Sums F) # x1) . 0 ) = 1 by A25, A11, A12, FUNCT_3:def 3;

        end;

        then

         A26: P2[ 0 ];

        

         A27: for k be Nat st P2[k] holds P2[(k + 1)]

        proof

          let k be Nat;

          assume

           A28: P2[k];

          assume

           A29: (k + 1) >= n;

          

           A30: ((( Partial_Sums F) # x1) . (k + 1)) = (( Partial_Sums (F # x1)) . (k + 1)) by A3, A9, A20, MESFUNC9:def 5, MESFUNC9: 32

          .= ((( Partial_Sums (F # x1)) . k) + ((F # x1) . (k + 1))) by MESFUNC9:def 1;

          per cases ;

            suppose

             A31: k >= n;

            then (k + 1) > n by NAT_1: 13;

            then ((F . (k + 1)) . x1) = 0 by A15;

            then ((F # x1) . (k + 1)) = 0 by MESFUNC5:def 13;

            then ((( Partial_Sums F) # x1) . (k + 1)) = (( Partial_Sums (F # x1)) . k) by A30, XXREAL_3: 4;

            hence ((( Partial_Sums F) # x1) . (k + 1)) = 1 by A28, A31, A3, A9, A20, MESFUNC9:def 5, MESFUNC9: 32;

          end;

            suppose

             A33: k < n;

            then

             A34: (k + 1) = n by A29, NAT_1: 8;

            ((( Partial_Sums F) # x1) . k) = 0 by A23, A33;

            then (( Partial_Sums (F # x1)) . k) = 0 by A3, A9, A20, MESFUNC9:def 5, MESFUNC9: 32;

            

            then ((( Partial_Sums F) # x1) . (k + 1)) = ((F # x1) . (k + 1)) by A30, XXREAL_3: 4

            .= ((F . (k + 1)) . x1) by MESFUNC5:def 13

            .= (( chi ((f . (k + 1)),X)) . x) by A1;

            hence ((( Partial_Sums F) # x1) . (k + 1)) = 1 by A34, A11, A12, FUNCT_3:def 3;

          end;

        end;

        

         A35: for k be Nat holds P2[k] from NAT_1:sch 2( A26, A27);

        for k be Nat holds (((( Partial_Sums F) # x1) ^\ n) . k) = 1

        proof

          let k be Nat;

          (((( Partial_Sums F) # x1) ^\ n) . k) = ((( Partial_Sums F) # x1) . (n + k)) by NAT_1:def 3;

          hence thesis by A35, NAT_1: 12;

        end;

        then ((( Partial_Sums F) # x1) ^\ n) is convergent_to_finite_number & ( lim ((( Partial_Sums F) # x1) ^\ n)) = 1 by MESFUNC5: 52;

        then (( lim ( Partial_Sums F)) . x) = 1 by A14, RINFSUP2: 16;

        hence (( chi (( Union f),X)) . x) = (( lim ( Partial_Sums F)) . x) by A10, A2, FUNCT_3:def 3;

      end;

        suppose

         A37: not x in ( Union f);

        then not x in ( union ( rng f)) by CARD_3:def 4;

        then

         A38: for V be set st V in ( rng f) holds not x in V by TARSKI:def 4;

        defpred P3[ Nat] means ((( Partial_Sums F) # x1) . $1) = 0 ;

        

         A39: ((( Partial_Sums F) # x1) . 0 ) = ((( Partial_Sums F) . 0 ) . x1) by MESFUNC5:def 13

        .= ((F . 0 ) . x1) by MESFUNC9:def 4

        .= (( chi ((f . 0 ),X)) . x1) by A1;

         not x in (f . 0 ) by A38, FUNCT_2: 4;

        then

         A40: P3[ 0 ] by A39, FUNCT_3:def 3;

        

         A41: for k be Nat st P3[k] holds P3[(k + 1)]

        proof

          let k be Nat;

          assume P3[k];

          then

           A42: (( Partial_Sums (F # x1)) . k) = 0 by A3, A9, A20, MESFUNC9:def 5, MESFUNC9: 32;

          

           A43: ((( Partial_Sums F) # x1) . (k + 1)) = (( Partial_Sums (F # x1)) . (k + 1)) by A3, A9, A20, MESFUNC9:def 5, MESFUNC9: 32

          .= ((( Partial_Sums (F # x1)) . k) + ((F # x1) . (k + 1))) by MESFUNC9:def 1

          .= ((F # x1) . (k + 1)) by A42, XXREAL_3: 4

          .= ((F . (k + 1)) . x1) by MESFUNC5:def 13

          .= (( chi ((f . (k + 1)),X)) . x) by A1;

           not x in (f . (k + 1)) by A38, FUNCT_2: 4;

          hence P3[(k + 1)] by A43, FUNCT_3:def 3;

        end;

        for k be Nat holds P3[k] from NAT_1:sch 2( A40, A41);

        then (( Partial_Sums F) # x1) is convergent_to_finite_number & ( lim (( Partial_Sums F) # x1)) = 0 by MESFUNC5: 52;

        hence (( chi (( Union f),X)) . x) = (( lim ( Partial_Sums F)) . x) by A37, A14, FUNCT_3:def 3;

      end;

    end;

    theorem :: MEASUR10:27

    

     Th27: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , r be Real st ( dom f) in S & 0 <= r & (for x be object st x in ( dom f) holds (f . x) = r) holds ( Integral (M,f)) = (r * (M . ( dom f)))

    proof

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

      assume that

       A1: ( dom f) in S & 0 <= r and

       A2: for x be object st x in ( dom f) holds (f . x) = r;

      now

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A3: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

        y = r by A2, A3;

        hence y in REAL by XREAL_0:def 1;

      end;

      then ( rng f) c= REAL ;

      then

      reconsider g = f as PartFunc of X, REAL by RELSET_1: 6;

      

       A4: ( Integral (M,g)) = (r * (M . ( dom g))) by A1, A2, MESFUNC6: 97;

      f = ( R_EAL g) by MESFUNC5:def 7;

      hence thesis by A4, MESFUNC6:def 3;

    end;

    theorem :: MEASUR10:28

    

     Th28: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A be Element of S st (ex E be Element of S st E = ( dom f) & f is E -measurable) & (for x be object st x in (( dom f) \ A) holds (f . x) = 0 ) & f is nonnegative holds ( Integral (M,f)) = ( Integral (M,(f | A)))

    proof

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

      assume that

       A1: ex E be Element of S st E = ( dom f) & f is E -measurable and

       A2: for x be object st x in (( dom f) \ A) holds (f . x) = 0 and

       A3: f is nonnegative;

      consider E be Element of S such that

       A4: E = ( dom f) & f is E -measurable by A1;

      reconsider B = (E \ A) as Element of S;

      

       A6: ( Integral (M,(f | (A \/ B)))) = (( Integral (M,(f | A))) + ( Integral (M,(f | B)))) by A1, A3, MESFUNC5: 91, XBOOLE_1: 79;

      (A \/ B) = (( dom f) \/ A) by A4, XBOOLE_1: 39;

      then

       A7: (f | (A \/ B)) = f by RELAT_1: 68, XBOOLE_1: 7;

      

       A8: B c= ( dom f) by A4, XBOOLE_1: 36;

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

      then

       A9: ( dom (f | B)) = B by A4, XBOOLE_1: 28, XBOOLE_1: 36;

      now

        let x be object;

        assume

         A10: x in ( dom (f | B));

        

        then ((f | B) . x) = ((f | B) /. x) by PARTFUN1:def 6

        .= (f /. x) by A10, PARTFUN1: 80

        .= (f . x) by A10, A8, A9, PARTFUN1:def 6;

        hence ((f | B) . x) = 0 by A2, A10, A9, A4;

      end;

      

      then ( Integral (M,(f | B))) = ( 0 * (M . ( dom (f | B)))) by A9, Th27

      .= 0 ;

      hence thesis by A6, A7, XXREAL_3: 4;

    end;

    theorem :: MEASUR10:29

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X, ExtREAL , A be Element of S st f is_integrable_on M & (for x be object st x in (( dom f) \ A) holds (f . x) = 0 ) holds ( Integral (M,f)) = ( Integral (M,(f | A)))

    proof

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

      assume that

       A1: f is_integrable_on M and

       A2: for x be object st x in (( dom f) \ A) holds (f . x) = 0 ;

      consider E be Element of S such that

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

      reconsider B = (E \ A) as Element of S;

      

       A4: ( Integral (M,(f | (A \/ B)))) = (( Integral (M,(f | A))) + ( Integral (M,(f | B)))) by A1, MESFUNC5: 98, XBOOLE_1: 79;

      (A \/ B) = (( dom f) \/ A) by A3, XBOOLE_1: 39;

      then

       A5: (f | (A \/ B)) = f by RELAT_1: 68, XBOOLE_1: 7;

      

       A6: B c= ( dom f) by A3, XBOOLE_1: 36;

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

      then

       A7: ( dom (f | B)) = B by A3, XBOOLE_1: 28, XBOOLE_1: 36;

      now

        let x be object;

        assume

         A9: x in ( dom (f | B));

        

        then ((f | B) . x) = ((f | B) /. x) by PARTFUN1:def 6

        .= (f /. x) by A9, PARTFUN1: 80

        .= (f . x) by A9, A7, A6, PARTFUN1:def 6;

        hence ((f | B) . x) = 0 by A2, A9, A7, A3;

      end;

      

      then ( Integral (M,(f | B))) = ( 0 * (M . ( dom (f | B)))) by A7, Th27

      .= 0 ;

      hence ( Integral (M,f)) = ( Integral (M,(f | A))) by A4, A5, XXREAL_3: 4;

    end;

    theorem :: MEASUR10:30

    

     Th30: for X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M2 be sigma_Measure of S2, D be Function of NAT , S1, E be Function of NAT , S2, A be Element of S1, B be Element of S2, F be Functional_Sequence of X2, ExtREAL , RD be sequence of ( Funcs (X1, REAL )), x be Element of X1 st (for n be Nat holds (RD . n) = ( chi ((D . n),X1))) & (for n be Nat holds (F . n) = (((RD . n) . x) (#) ( chi ((E . n),X2)))) & (for n be Nat holds (E . n) c= B) holds ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x))) & I is summable & ( Integral (M2,( lim ( Partial_Sums F)))) = ( Sum I)

    proof

      let X1,X2 be non empty set, S1 be SigmaField of X1, S2 be SigmaField of X2, M2 be sigma_Measure of S2, D be Function of NAT , S1, E be Function of NAT , S2, A be Element of S1, B be Element of S2, F be Functional_Sequence of X2, ExtREAL , RD be sequence of ( Funcs (X1, REAL )), x be Element of X1;

      assume that

       A7: (for n be Nat holds (RD . n) = ( chi ((D . n),X1))) and

       A8: (for n be Nat holds (F . n) = (((RD . n) . x) (#) ( chi ((E . n),X2)))) and

       A9: (for n be Nat holds (E . n) c= B);

      

       B1: for n be Nat holds ( dom (F . n)) = X2

      proof

        let n be Nat;

        ( dom (F . n)) = ( dom (((RD . n) . x) (#) ( chi ((E . n),X2)))) by A8;

        then ( dom (F . n)) = ( dom ( chi ((E . n),X2))) by MESFUNC1:def 6;

        hence ( dom (F . n)) = X2 by FUNCT_3:def 3;

      end;

      reconsider SX2 = X2 as Element of S2 by PROB_1: 5;

      

       P1: ( dom (F . 0 )) = X2 by B1;

      

       B2: for n be Nat, y be set st y in (E . n) holds ((F . n) . y) = 0 or ((F . n) . y) = 1

      proof

        let n be Nat, y be set;

        assume

         B3: y in (E . n);

        

         B4: (E . n) in S2;

        then y in X2 by B3;

        then

         B5: y in ( dom (F . n)) by B1;

        then

         B6: ((F . n) . y) in ( rng (F . n)) by FUNCT_1: 3;

        reconsider y1 = y as Element of X2 by B3, B4;

         B7:

        now

          assume x in (D . n);

          then (( chi ((D . n),X1)) . x) = 1 by FUNCT_3:def 3;

          then ((RD . n) . x) = 1 by A7;

          then (F . n) = (1 (#) ( chi ((E . n),X2))) by A8;

          then (F . n) = ( chi ((E . n),X2)) by MESFUNC2: 1;

          then ( rng (F . n)) c= { 0 , 1} by FUNCT_3: 39;

          hence ((F . n) . y) = 0 or ((F . n) . y) = 1 by B6, TARSKI:def 2;

        end;

        now

          assume not x in (D . n);

          then (( chi ((D . n),X1)) . x) = 0 by FUNCT_3:def 3;

          then ((RD . n) . x) = 0 by A7;

          then (F . n) = ( 0 (#) ( chi ((E . n),X2))) by A8;

          then ((F . n) . y) = ( 0 * (( chi ((E . n),X2)) . y1)) by B5, MESFUNC1:def 6;

          hence ((F . n) . y) = 0 ;

        end;

        hence ((F . n) . y) = 0 or ((F . n) . y) = 1 by B7;

      end;

      

       B8: for n be Nat, y be set st not y in (E . n) holds ((F . n) . y) = 0

      proof

        let n be Nat, y be set;

        assume

         B9: not y in (E . n);

         B10:

        now

          assume

           B11: y in X2;

          then

          reconsider y1 = y as Element of X2;

          

           B12: (( chi ((E . n),X2)) . y1) = 0 by B9, FUNCT_3:def 3;

          

           B13: y in ( dom (F . n)) by B1, B11;

          (F . n) = (((RD . n) . x) (#) ( chi ((E . n),X2))) by A8;

          then ((F . n) . y) = (((RD . n) . x) * (( chi ((E . n),X2)) . y1)) by B13, MESFUNC1:def 6;

          hence ((F . n) . y) = 0 by B12;

        end;

        now

          assume not y in X2;

          then not y in ( dom (F . n));

          hence ((F . n) . y) = 0 by FUNCT_1:def 2;

        end;

        hence ((F . n) . y) = 0 by B10;

      end;

       P2:

      now

        let n,m be Nat;

        assume n <> m;

        thus for y be set st y in (( dom (F . n)) /\ ( dom (F . m))) holds ((F . n) . y) <> +infty or ((F . m) . y) <> -infty

        proof

          let y be set;

          assume y in (( dom (F . n)) /\ ( dom (F . m)));

          y in (E . n) implies ((F . n) . y) <> +infty or ((F . m) . y) <> -infty by B2;

          hence ((F . n) . y) <> +infty or ((F . m) . y) <> -infty by B8;

        end;

      end;

      then

       S2: F is additive by MESFUNC9:def 5;

      now

        let n,m be Nat;

        ( dom (F . n)) = X2 & ( dom (F . m)) = X2 by B1;

        hence ( dom (F . n)) = ( dom (F . m));

      end;

      then

       P3: F is with_the_same_dom by MESFUNC8:def 2;

      

       P4: for n be Nat holds (F . n) is nonnegative & (F . n) is B -measurable

      proof

        let n be Nat;

        now

          let y be object;

          per cases ;

            suppose not y in ( dom (F . n));

            hence ((F . n) . y) >= 0 by FUNCT_1:def 2;

          end;

            suppose y in ( dom (F . n)) & y in (E . n);

            hence ((F . n) . y) >= 0 by B2;

          end;

            suppose y in ( dom (F . n)) & not y in (E . n);

            hence ((F . n) . y) >= 0 by B8;

          end;

        end;

        hence (F . n) is nonnegative by SUPINF_2: 51;

        thus (F . n) is B -measurable

        proof

          

           B14: ( dom ( chi ((E . n),X2))) = X2 by FUNCT_3:def 3;

          per cases ;

            suppose x in (D . n);

            then (( chi ((D . n),X1)) . x) = 1 by FUNCT_3:def 3;

            then ((RD . n) . x) = 1 by A7;

            then (F . n) = (1 (#) ( chi ((E . n),X2))) by A8;

            hence (F . n) is B -measurable by B14, MESFUNC1: 37, MESFUNC2: 29;

          end;

            suppose not x in (D . n);

            then (( chi ((D . n),X1)) . x) = 0 by FUNCT_3:def 3;

            then ((RD . n) . x) = 0 by A7;

            then (F . n) = ( 0 (#) ( chi ((E . n),X2))) by A8;

            hence (F . n) is B -measurable by B14, MESFUNC1: 37, MESFUNC2: 29;

          end;

        end;

      end;

      for y be Element of X2 st y in B holds (F # y) is summable

      proof

        let y be Element of X2;

        assume y in B;

        for n be Element of NAT holds 0 <= ((F # y) . n)

        proof

          let n be Element of NAT ;

          ((F # y) . n) = ((F . n) . y) by MESFUNC5:def 13;

          hence 0 <= ((F # y) . n) by P4, SUPINF_2: 51;

        end;

        then (F # y) is nonnegative by SUPINF_2: 39;

        then ( Partial_Sums (F # y)) is non-decreasing by MESFUNC9: 16;

        hence (F # y) is summable by RINFSUP2: 37, MESFUNC9:def 2;

      end;

      then

      consider I be ExtREAL_sequence such that

       Q1: (for n be Nat holds (I . n) = ( Integral (M2,((F . n) | B)))) & I is summable & ( Integral (M2,(( lim ( Partial_Sums F)) | B))) = ( Sum I) by P1, P2, P3, P4, MESFUNC9:def 5, MESFUNC9: 51;

      take I;

      

       R1: for n be Nat holds ( chi ((E . n),X2)) is SX2 -measurable by MESFUNC2: 29;

      

       Q2: for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x))

      proof

        let n be Nat;

        

         B16: (I . n) = ( Integral (M2,((F . n) | B))) by Q1;

        

         B17: ( dom ((F . n) | B)) = (( dom (F . n)) /\ B) by RELAT_1: 61;

        then

         B18: ( dom ((F . n) | B)) = (X2 /\ B) by B1;

        

         B19: ( dom (((RD . n) . x) (#) (( chi ((E . n),X2)) | B))) = ( dom (( chi ((E . n),X2)) | B)) by MESFUNC1:def 6

        .= (( dom ( chi ((E . n),X2))) /\ B) by RELAT_1: 61

        .= (X2 /\ B) by FUNCT_3:def 3;

        now

          let y be object;

          assume

           B20: y in ( dom ((F . n) | B));

          then

          reconsider y1 = y as Element of X2;

          

           B22: y in X2 & y in B by B17, B20, XBOOLE_0:def 4;

          ( dom ( chi ((E . n),X2))) = X2 by FUNCT_3:def 3;

          then

           B23: y in ( dom (((RD . n) . x) (#) ( chi ((E . n),X2)))) by B22, MESFUNC1:def 6;

          

           B21: (((F . n) | B) . y) = ((F . n) . y1) by B20, FUNCT_1: 47

          .= ((((RD . n) . x) (#) ( chi ((E . n),X2))) . y1) by A8

          .= (((RD . n) . x) * (( chi ((E . n),X2)) . y)) by B23, MESFUNC1:def 6;

          ((((RD . n) . x) (#) (( chi ((E . n),X2)) | B)) . y) = (((RD . n) . x) * ((( chi ((E . n),X2)) | B) . y)) by B20, B18, B19, MESFUNC1:def 6

          .= (((RD . n) . x) * (( chi ((E . n),X2)) . y)) by B22, FUNCT_1: 49;

          hence (((F . n) | B) . y) = ((((RD . n) . x) (#) (( chi ((E . n),X2)) | B)) . y) by B21;

        end;

        then

         B24: (I . n) = ( Integral (M2,(((RD . n) . x) (#) (( chi ((E . n),X2)) | B)))) by B16, B18, B19, FUNCT_1:def 11;

        

         C0: B = ( dom (((RD . n) . x) (#) (( chi ((E . n),X2)) | B))) by B19, XBOOLE_1: 28;

        

         C4: ( dom (( chi ((E . n),X2)) | B)) = (( dom ( chi ((E . n),X2))) /\ B) by RELAT_1: 61;

        (( dom ( chi ((E . n),X2))) /\ B) = (X2 /\ B) by FUNCT_3:def 3;

        then

         C3: (( dom ( chi ((E . n),X2))) /\ B) = B by XBOOLE_1: 28;

        then

         C8: (( chi ((E . n),X2)) | B) is B -measurable by MESFUNC2: 29, MESFUNC5: 42;

        

         C5a: (( chi ((E . n),X2)) | B) is nonnegative by MESFUNC5: 15;

         C6:

        now

          assume x in (D . n);

          then (( chi ((D . n),X1)) . x) = 1 by FUNCT_3:def 3;

          hence ((RD . n) . x) = 1 by A7;

        end;

         C7:

        now

          assume not x in (D . n);

          then (( chi ((D . n),X1)) . x) = 0 by FUNCT_3:def 3;

          hence ((RD . n) . x) = 0 by A7;

        end;

        then (((RD . n) . x) (#) (( chi ((E . n),X2)) | B)) is nonnegative by C5a, C6, MESFUNC5: 20;

        then (I . n) = ( integral+ (M2,(((RD . n) . x) (#) (( chi ((E . n),X2)) | B)))) by B24, C0, C8, C3, C4, MESFUNC1: 37, MESFUNC5: 88;

        then (I . n) = (((RD . n) . x) * ( integral+ (M2,(( chi ((E . n),X2)) | B)))) by C3, C4, C6, C7, C8, MESFUNC5: 15, MESFUNC5: 86;

        then

         D2: (I . n) = (((RD . n) . x) * ( Integral (M2,(( chi ((E . n),X2)) | B)))) by C3, C4, C8, MESFUNC5: 15, MESFUNC5: 88;

        

         E1: ( dom ( chi ((E . n),X2))) = X2 by FUNCT_3:def 3;

        for y be object st y in (( dom ( chi ((E . n),X2))) \ B) holds (( chi ((E . n),X2)) . y) = 0

        proof

          let y be object;

          assume

           E4: y in (( dom ( chi ((E . n),X2))) \ B);

          then

          reconsider y1 = y as Element of X2;

          (E . n) c= B by A9;

          then not y1 in (E . n) by E4, XBOOLE_0:def 5;

          hence (( chi ((E . n),X2)) . y) = 0 by FUNCT_3:def 3;

        end;

        then ( Integral (M2,( chi ((E . n),X2)))) = ( Integral (M2,(( chi ((E . n),X2)) | B))) by E1, R1, Th28;

        then (I . n) = ((M2 . (E . n)) * ((RD . n) . x)) by D2, MESFUNC9: 14;

        hence (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x)) by A7;

      end;

      

       F1: ( dom ( lim ( Partial_Sums F))) = ( dom (( Partial_Sums F) . 0 )) by MESFUNC8:def 9

      .= ( dom (F . 0 )) by MESFUNC9:def 4;

      then

       F4: ( dom ( lim ( Partial_Sums F))) = SX2 by B1;

      

       G0: ( Partial_Sums F) is with_the_same_dom Functional_Sequence of X2, ExtREAL by P2, P3, MESFUNC9:def 5, MESFUNC9: 43;

      

       G1: ( dom (( Partial_Sums F) . 0 )) = ( dom (F . 0 )) by MESFUNC9:def 4

      .= SX2 by B1;

      

       R2: for n be Nat holds (F . n) is SX2 -measurable

      proof

        let n be Nat;

        ( chi ((E . n),X2)) is SX2 -measurable & ( dom ( chi ((E . n),X2))) = SX2 by MESFUNC2: 29, FUNCT_3:def 3;

        then (((RD . n) . x) (#) ( chi ((E . n),X2))) is SX2 -measurable by MESFUNC1: 37;

        hence (F . n) is SX2 -measurable by A8;

      end;

      for n be Nat holds (F . n) is without-infty

      proof

        let n be Nat;

        (F . n) is nonnegative by P4;

        hence (F . n) is without-infty;

      end;

      then

       G2: for n be Nat holds (( Partial_Sums F) . n) is SX2 -measurable by R2, MESFUNC9: 41;

      for y be Element of X2 st y in SX2 holds (( Partial_Sums F) # y) is convergent

      proof

        let y be Element of X2;

        assume y in SX2;

        then y in ( dom (F . 0 )) by B1;

        hence (( Partial_Sums F) # y) is convergent by P3, P4, MESFUNC9: 38;

      end;

      then

       F2: ( lim ( Partial_Sums F)) is SX2 -measurable by G0, G1, G2, MESFUNC8: 25;

      

       F3: for y be object st y in (( dom ( lim ( Partial_Sums F))) \ B) holds (( lim ( Partial_Sums F)) . y) = 0

      proof

        let y be object;

        assume

         K0: y in (( dom ( lim ( Partial_Sums F))) \ B);

        then

         K1: y in ( dom ( lim ( Partial_Sums F))) & not y in B by XBOOLE_0:def 5;

        then y in ( dom (( Partial_Sums F) . 0 )) by MESFUNC8:def 9;

        then

         J1: y in ( dom (F . 0 )) by MESFUNC9:def 4;

        reconsider y1 = y as Element of X2 by K0;

        

         K2: (( lim ( Partial_Sums F)) . y) = ( lim (( Partial_Sums F) # y1)) by K1, MESFUNC8:def 9;

        for n be Nat holds ((( Partial_Sums F) # y1) . n) = 0

        proof

          let n be Nat;

          

           K6: ((( Partial_Sums F) # y1) . n) = ((( Partial_Sums F) . n) . y1) by MESFUNC5:def 13;

          defpred P[ Nat] means ((( Partial_Sums F) . $1) . y1) = 0 ;

          

           K3: ((( Partial_Sums F) . 0 ) . y1) = ((F . 0 ) . y1) by MESFUNC9:def 4;

          (E . 0 ) c= B by A9;

          then

           K4: P[ 0 ] by K1, K3, B8;

          

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

          proof

            let k be Nat;

            assume

             J2: P[k];

            

             J3: ( dom (( Partial_Sums F) . (k + 1))) = ( dom (( Partial_Sums F) . 0 )) by S2, P3, MESFUNC9: 43, MESFUNC8:def 2

            .= ( dom (F . 0 )) by MESFUNC9:def 4;

            

             J4: (E . (k + 1)) c= B by A9;

            (( Partial_Sums F) . (k + 1)) = ((( Partial_Sums F) . k) + (F . (k + 1))) by MESFUNC9:def 4;

            

            then ((( Partial_Sums F) . (k + 1)) . y1) = (((( Partial_Sums F) . k) . y1) + ((F . (k + 1)) . y1)) by J1, J3, MESFUNC1:def 3

            .= ((F . (k + 1)) . y1) by J2, XXREAL_3: 4;

            hence P[(k + 1)] by J4, B8, K1;

          end;

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

          hence ((( Partial_Sums F) # y1) . n) = 0 by K6;

        end;

        hence (( lim ( Partial_Sums F)) . y) = 0 by K2, MESFUNC5: 52;

      end;

      for y be object st y in ( dom ( lim ( Partial_Sums F))) holds (( lim ( Partial_Sums F)) . y) >= 0

      proof

        let y be object;

        assume

         L1: y in ( dom ( lim ( Partial_Sums F)));

        then

        reconsider y1 = y as Element of X2;

        

         L2: for n be Nat holds ((( Partial_Sums F) # y1) . n) >= 0

        proof

          let n be Nat;

          ((( Partial_Sums F) . n) . y1) >= 0 by P4, MESFUNC9: 36, SUPINF_2: 51;

          hence ((( Partial_Sums F) # y1) . n) >= 0 by MESFUNC5:def 13;

        end;

        ( lim (( Partial_Sums F) # y1)) >= 0 by L1, F1, L2, P3, P4, MESFUNC9: 10, MESFUNC9: 38;

        hence (( lim ( Partial_Sums F)) . y) >= 0 by L1, MESFUNC8:def 9;

      end;

      hence thesis by Q1, Q2, F4, F2, F3, Th28, SUPINF_2: 52;

    end;

    theorem :: MEASUR10:31

    for X be non empty set, S be SigmaField of X, A be Element of S, p be R_eal holds (X --> p) is A -measurable

    proof

      let X be non empty set, S be SigmaField of X, A be Element of S, p be R_eal;

      

       A0: ( dom (X --> p)) = X by FUNCOP_1: 13;

      for r be Real holds (A /\ ( great_eq_dom ((X --> p),r))) in S

      proof

        let r be Real;

        per cases ;

          suppose

           A2: r > p;

          for x be object holds not x in ( great_eq_dom ((X --> p),r))

          proof

            let x be object;

            hereby

              assume x in ( great_eq_dom ((X --> p),r));

              then x in ( dom (X --> p)) & r <= ((X --> p) . x) by MESFUNC1:def 14;

              hence contradiction by A2, FUNCOP_1: 7;

            end;

          end;

          then ( great_eq_dom ((X --> p),r)) = {} by XBOOLE_0:def 1;

          hence (A /\ ( great_eq_dom ((X --> p),r))) in S by MEASURE1: 7;

        end;

          suppose

           A4: r <= p;

          now

            let x be object;

            assume

             A6: x in X;

            then ((X --> p) . x) = p by FUNCOP_1: 7;

            hence x in ( great_eq_dom ((X --> p),r)) by A0, A4, A6, MESFUNC1:def 14;

          end;

          then X c= ( great_eq_dom ((X --> p),r));

          then ( great_eq_dom ((X --> p),r)) = X;

          then (A /\ ( great_eq_dom ((X --> p),r))) = A by XBOOLE_1: 28;

          hence (A /\ ( great_eq_dom ((X --> p),r))) in S;

        end;

      end;

      hence thesis by A0, MESFUNC1: 27;

    end;

    definition

      let A,X be set;

      :: MEASUR10:def7

      func Xchi (A,X) -> Function of X, ExtREAL means

      : DefXchi: for x be object st x in X holds (x in A implies (it . x) = +infty ) & ( not x in A implies (it . x) = 0 );

      existence

      proof

        defpred P[ object, object] means ($1 in A implies $2 = +infty ) & ( not $1 in A implies $2 = 0 );

        

         A1: for x be object st x in X holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in X;

           not x in A implies ex y be object st y = {} & (x in A implies y = +infty ) & ( not x in A implies y = {} );

          hence thesis;

        end;

        

         A2: for x,y1,y2 be object st x in X & P[x, y1] & P[x, y2] holds y1 = y2;

        consider f be Function such that

         A3: ( dom f) = X & for x be object st x in X holds P[x, (f . x)] from FUNCT_1:sch 2( A2, A1);

        for x be object st x in X holds (f . x) in ExtREAL

        proof

          let x be object;

          assume

           A4: x in X;

          per cases ;

            suppose x in A;

            then (f . x) = +infty by A3, A4;

            hence (f . x) in ExtREAL ;

          end;

            suppose not x in A;

            then (f . x) = 0. by A3, A4;

            hence (f . x) in ExtREAL ;

          end;

        end;

        then

        reconsider f as Function of X, ExtREAL by A3, FUNCT_2: 3;

        take f;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let f1,f2 be Function of X, ExtREAL such that

         A4: for x be object st x in X holds (x in A implies (f1 . x) = +infty ) & ( not x in A implies (f1 . x) = 0 ) and

         A6: for x be object st x in X holds (x in A implies (f2 . x) = +infty ) & ( not x in A implies (f2 . x) = 0 );

        for x be object st x in X holds (f1 . x) = (f2 . x)

        proof

          let x be object;

          assume

           A7: x in X;

          then

           A8: not x in A implies (f1 . x) = 0 & (f2 . x) = 0 by A4, A6;

          x in A implies (f1 . x) = +infty & (f2 . x) = +infty by A4, A6, A7;

          hence thesis by A8;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    

     Lm08: for X be non empty set, S be SigmaField of X, A be Element of S, r be Real st r > 0 holds ( great_eq_dom (( Xchi (A,X)),r)) = A

    proof

      let X be non empty set, S be SigmaField of X, A be Element of S, r be Real;

      assume

       A1: r > 0 ;

      now

        let x be object;

        assume

         A2: x in A;

        then x in X;

        then

         A4: x in ( dom ( Xchi (A,X))) by FUNCT_2:def 1;

        (( Xchi (A,X)) . x) = +infty by A2, DefXchi;

        then r <= (( Xchi (A,X)) . x) by XXREAL_0: 3;

        hence x in ( great_eq_dom (( Xchi (A,X)),r)) by A4, MESFUNC1:def 14;

      end;

      then

       A5: A c= ( great_eq_dom (( Xchi (A,X)),r));

      now

        let x be object;

        assume x in ( great_eq_dom (( Xchi (A,X)),r));

        then x in ( dom ( Xchi (A,X))) & r <= (( Xchi (A,X)) . x) by MESFUNC1:def 14;

        hence x in A by A1, DefXchi;

      end;

      then ( great_eq_dom (( Xchi (A,X)),r)) c= A;

      hence thesis by A5;

    end;

    

     Lm09: for X be non empty set, S be SigmaField of X, A be Element of S, r be Real st r <= 0 holds ( great_eq_dom (( Xchi (A,X)),r)) = X

    proof

      let X be non empty set, S be SigmaField of X, A be Element of S, r be Real;

      assume

       A1: r <= 0 ;

      now

        let x be object;

        assume

         A2: x in X;

        then

         A3: x in ( dom ( Xchi (A,X))) by FUNCT_2:def 1;

        per cases ;

          suppose x in A;

          then (( Xchi (A,X)) . x) = +infty by DefXchi;

          then r <= (( Xchi (A,X)) . x) by XXREAL_0: 3;

          hence x in ( great_eq_dom (( Xchi (A,X)),r)) by A3, MESFUNC1:def 14;

        end;

          suppose not x in A;

          then (( Xchi (A,X)) . x) = 0 by A2, DefXchi;

          hence x in ( great_eq_dom (( Xchi (A,X)),r)) by A1, A3, MESFUNC1:def 14;

        end;

      end;

      then X c= ( great_eq_dom (( Xchi (A,X)),r));

      hence thesis;

    end;

    theorem :: MEASUR10:32

    

     Th32: for X be non empty set, S be SigmaField of X, A,B be Element of S holds ( Xchi (A,X)) is B -measurable

    proof

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

      

       A1: ( dom ( Xchi (A,X))) = X by FUNCT_2:def 1;

      for r be Real holds (B /\ ( great_eq_dom (( Xchi (A,X)),r))) in S

      proof

        let r be Real;

        per cases ;

          suppose r > 0 ;

          then (B /\ ( great_eq_dom (( Xchi (A,X)),r))) = (B /\ A) by Lm08;

          hence (B /\ ( great_eq_dom (( Xchi (A,X)),r))) in S;

        end;

          suppose r <= 0 ;

          then ( great_eq_dom (( Xchi (A,X)),r)) = X by Lm09;

          then (B /\ ( great_eq_dom (( Xchi (A,X)),r))) = B by XBOOLE_1: 28;

          hence (B /\ ( great_eq_dom (( Xchi (A,X)),r))) in S;

        end;

      end;

      hence thesis by A1, MESFUNC1: 27;

    end;

    registration

      let X be non empty set;

      let S be SigmaField of X;

      let A be Element of S;

      cluster ( Xchi (A,X)) -> A -measurable;

      coherence by Th32;

    end

    registration

      let X,A be set;

      cluster ( Xchi (A,X)) -> nonnegative;

      coherence

      proof

        for x be object holds (( Xchi (A,X)) . x) >= 0

        proof

          let x be object;

          per cases ;

            suppose

             L1: x in X;

            per cases ;

              suppose x in A;

              hence (( Xchi (A,X)) . x) >= 0 by L1, DefXchi;

            end;

              suppose not x in A;

              hence (( Xchi (A,X)) . x) >= 0 by L1, DefXchi;

            end;

          end;

            suppose not x in X;

            then not x in ( dom ( Xchi (A,X)));

            hence (( Xchi (A,X)) . x) >= 0 by FUNCT_1:def 2;

          end;

        end;

        hence ( Xchi (A,X)) is nonnegative by SUPINF_2: 51;

      end;

    end

    theorem :: MEASUR10:33

    

     Th34: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, A be Element of S holds ((M . A) <> 0 implies ( Integral (M,( Xchi (A,X)))) = +infty ) & ((M . A) = 0 implies ( Integral (M,( Xchi (A,X)))) = 0 )

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, A be Element of S;

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

      

       N6: XX = ( dom ( Xchi (A,X))) by FUNCT_2:def 1;

      hereby

        assume

         Q1: (M . A) <> 0 ;

        now

          let x be object;

          assume x in ( eq_dom (( Xchi (A,X)), +infty ));

          then x in ( dom ( Xchi (A,X))) & (( Xchi (A,X)) . x) = +infty by MESFUNC1:def 15;

          hence x in A by DefXchi;

        end;

        then

         Q3: ( eq_dom (( Xchi (A,X)), +infty )) c= A;

        now

          let x be object;

          assume

           Q4: x in A;

          then x in X;

          then

           Q6: x in ( dom ( Xchi (A,X))) by FUNCT_2:def 1;

          (( Xchi (A,X)) . x) = +infty by Q4, DefXchi;

          hence x in ( eq_dom (( Xchi (A,X)), +infty )) by Q6, MESFUNC1:def 15;

        end;

        then A c= ( eq_dom (( Xchi (A,X)), +infty ));

        then

         WW: (XX /\ ( eq_dom (( Xchi (A,X)), +infty ))) = A by Q3, XBOOLE_1: 28;

        ( Xchi (A,X)) is XX -measurable by Th32;

        hence ( Integral (M,( Xchi (A,X)))) = +infty by Q1, N6, MESFUNC9: 13, WW;

      end;

      assume

       M5: (M . A) = 0 ;

      reconsider XDn = (XX \ A) as Element of S;

      reconsider F = (( Xchi (A,X)) | A) as PartFunc of X, ExtREAL by PARTFUN1: 11;

      reconsider F1 = (( Xchi (A,X)) | XDn) as PartFunc of X, ExtREAL by PARTFUN1: 11;

      reconsider F2 = (( Xchi (A,X)) | (XDn \/ A)) as PartFunc of X, ExtREAL by PARTFUN1: 11;

      

       ZZ: ex E be Element of S st E = ( dom ( Xchi (A,X))) & ( Xchi (A,X)) is E -measurable

      proof

        take XX;

        thus thesis by N6, Th32;

      end;

      then

       M4: ( Integral (M,F)) = 0 by M5, MESFUNC5: 94;

      

       N1: XDn = ( dom (( Xchi (A,X)) | XDn)) by FUNCT_2:def 1;

      

       MM: XDn = (( dom ( Xchi (A,X))) /\ XDn) by N6, XBOOLE_1: 28;

      ( Xchi (A,X)) is XDn -measurable by Th32;

      then

       N2: F1 is XDn -measurable by MM, MESFUNC5: 42;

      for x be Element of X st x in ( dom (( Xchi (A,X)) | XDn)) holds ((( Xchi (A,X)) | XDn) . x) = 0

      proof

        let x be Element of X;

        assume

         N31: x in ( dom (( Xchi (A,X)) | XDn));

        then not x in A by XBOOLE_0:def 5;

        then (( Xchi (A,X)) . x) = 0 by DefXchi;

        hence ((( Xchi (A,X)) | XDn) . x) = 0 by N31, FUNCT_1: 47;

      end;

      then

       N4: ( integral+ (M,F1)) = 0 by N1, N2, MESFUNC5: 87;

      

       N5: ( Integral (M,F1)) = 0 by N1, N2, N4, MESFUNC5: 15, MESFUNC5: 88;

      (XDn \/ A) = (XX \/ A) by XBOOLE_1: 39;

      then

       N10: (XDn \/ A) = XX by XBOOLE_1: 12;

      XDn misses A by XBOOLE_1: 79;

      then ( Integral (M,F2)) = (( Integral (M,F1)) + ( Integral (M,F))) by ZZ, MESFUNC5: 91;

      then ( Integral (M,F2)) = (( Integral (M,F1)) + 0 ) by M4;

      hence ( Integral (M,( Xchi (A,X)))) = 0 by N5, N10;

    end;

    theorem :: MEASUR10:34

    

     Th35: 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, K be disjoint_valued Function of NAT , ( measurable_rectangles (S1,S2)) st ( Union K) in ( measurable_rectangles (S1,S2)) holds (( product-pre-Measure (M1,M2)) . ( Union K)) = ( SUM (( product-pre-Measure (M1,M2)) * K))

    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, K be disjoint_valued Function of NAT , ( measurable_rectangles (S1,S2));

      assume

       A1: ( Union K) in ( measurable_rectangles (S1,S2));

      then

      consider A be Element of S1, B be Element of S2 such that

       A2: ( Union K) = [:A, B:];

      consider P be Element of S1, Q be Element of S2 such that

       Q1: ( Union K) = [:P, Q:] & (( product-pre-Measure (M1,M2)) . ( Union K)) = ((M1 . P) * (M2 . Q)) by A1, Def6;

      

       A10: A c= X1 & B c= X2;

      deffunc F0( object) = ( chi ((K . $1), [:X1, X2:]));

      consider XK be Functional_Sequence of [:X1, X2:], ExtREAL such that

       A3: for n be Nat holds (XK . n) = F0(n) from SEQFUNC:sch 1;

      

       K1: ( dom XK) = NAT by FUNCT_2:def 1;

      now

        let n be object;

        assume n in NAT ;

        then

        reconsider n1 = n as Nat;

        

         K2: (XK . n) = ( chi ((K . n1), [:X1, X2:])) by A3;

        

         K3: ( dom ( chi ((K . n1), [:X1, X2:]))) = [:X1, X2:] by FUNCT_3:def 3;

        ( rng ( chi ((K . n1), [:X1, X2:]))) c= ExtREAL ;

        hence (XK . n) in ( Funcs ( [:X1, X2:], ExtREAL )) by K2, K3, FUNCT_2:def 2;

      end;

      then

      reconsider XXK = XK as sequence of ( Funcs ( [:X1, X2:], ExtREAL )) by K1, FUNCT_2: 3;

      defpred P1[ Nat, object] means $2 = ( proj1 (K . $1));

      

       B0: for i be Element of NAT holds ex A be Element of S1 st P1[i, A]

      proof

        let i be Element of NAT ;

        (K . i) in ( measurable_rectangles (S1,S2));

        then

        consider Ai be Element of S1, Bi be Element of S2 such that

         B1: (K . i) = [:Ai, Bi:];

        per cases ;

          suppose

           B2: Bi <> {} ;

          take Ai;

          thus ( proj1 (K . i)) = Ai by B1, B2, FUNCT_5: 9;

        end;

          suppose

           B3: Bi = {} ;

          reconsider Ai = {} as Element of S1 by MEASURE1: 7;

          take Ai;

          thus ( proj1 (K . i)) = Ai by B3, B1;

        end;

      end;

      consider D be Function of NAT , S1 such that

       B4: for i be Element of NAT holds P1[i, (D . i)] from FUNCT_2:sch 3( B0);

      defpred P2[ Nat, object] means $2 = ( proj2 (K . $1));

      

       C0: for i be Element of NAT holds ex B be Element of S2 st P2[i, B]

      proof

        let i be Element of NAT ;

        (K . i) in ( measurable_rectangles (S1,S2));

        then

        consider Ai be Element of S1, Bi be Element of S2 such that

         C1: (K . i) = [:Ai, Bi:];

        per cases ;

          suppose

           C2: Ai <> {} ;

          take Bi;

          thus ( proj2 (K . i)) = Bi by C1, C2, FUNCT_5: 9;

        end;

          suppose

           C3: Ai = {} ;

          reconsider Bi = {} as Element of S2 by MEASURE1: 7;

          take Bi;

          thus ( proj2 (K . i)) = Bi by C1, C3;

        end;

      end;

      consider E be Function of NAT , S2 such that

       C4: for i be Element of NAT holds P2[i, (E . i)] from FUNCT_2:sch 3( C0);

      deffunc F1( object) = ( chi ((D . $1),X1));

      consider XD be Functional_Sequence of X1, ExtREAL such that

       B5: for n be Nat holds (XD . n) = F1(n) from SEQFUNC:sch 1;

      deffunc F2( object) = ( chi ((E . $1),X2));

      consider XE be Functional_Sequence of X2, ExtREAL such that

       C5: for n be Nat holds (XE . n) = F2(n) from SEQFUNC:sch 1;

      

       E0: for n be Nat, x,y be object st x in X1 & y in X2 holds ((XK . n) . (x,y)) = (((XD . n) . x) * ((XE . n) . y))

      proof

        let n be Nat, x,y be object;

        assume

         E1: x in X1 & y in X2;

        then

         E7: [x, y] in [:X1, X2:] by ZFMISC_1: 87;

        

         E5: (XK . n) = ( chi ((K . n), [:X1, X2:])) & (XD . n) = ( chi ((D . n),X1)) & (XE . n) = ( chi ((E . n),X2)) by A3, B5, C5;

        

         E2: n in NAT by ORDINAL1:def 12;

        (K . n) in ( measurable_rectangles (S1,S2));

        then

        consider An be Element of S1, Bn be Element of S2 such that

         E3: (K . n) = [:An, Bn:];

        

         E4: (D . n) = ( proj1 (K . n)) & (E . n) = ( proj2 (K . n)) by B4, C4, E2;

        per cases ;

          suppose x in An & y in Bn;

          then (D . n) = An & (E . n) = Bn by E4, E3, FUNCT_5: 9;

          hence ((XK . n) . (x,y)) = (((XD . n) . x) * ((XE . n) . y)) by E5, E3, E1, Th26;

        end;

          suppose not x in An or not y in Bn;

          then not [x, y] in [:An, Bn:] by ZFMISC_1: 87;

          then

           E8: ((XK . n) . (x,y)) = 0 by E7, E5, E3, FUNCT_3:def 3;

          per cases ;

            suppose [:An, Bn:] = {} ;

            then ((XD . n) . x) = 0 & ((XE . n) . y) = 0 by E4, E3, E5, E1, FUNCT_3:def 3;

            hence ((XK . n) . (x,y)) = (((XD . n) . x) * ((XE . n) . y)) by E8;

          end;

            suppose [:An, Bn:] <> {} ;

            then (D . n) = An & (E . n) = Bn by E4, E3, FUNCT_5: 9;

            hence ((XK . n) . (x,y)) = (((XD . n) . x) * ((XE . n) . y)) by E3, E5, E1, Th26;

          end;

        end;

      end;

      

       HH2: (( product-pre-Measure (M1,M2)) . ( Union K)) = ((M1 . A) * (M2 . B))

      proof

        per cases ;

          suppose A <> {} & B <> {} ;

          then A = P & B = Q by A2, Q1, ZFMISC_1: 110;

          hence (( product-pre-Measure (M1,M2)) . ( Union K)) = ((M1 . A) * (M2 . B)) by Q1;

        end;

          suppose

           HA: A = {} or B = {} ;

          then P = {} or Q = {} by A2, Q1;

          then ((M1 . A) = 0 or (M2 . B) = 0 ) & ((M1 . P) = 0 or (M2 . Q) = 0 ) by HA, VALUED_0:def 19;

          hence (( product-pre-Measure (M1,M2)) . ( Union K)) = ((M1 . A) * (M2 . B)) by Q1;

        end;

      end;

      

       T1: ( rng ( chi ( [:A, B:], [:X1, X2:]))) c= ExtREAL ;

      ( dom ( chi ( [:A, B:], [:X1, X2:]))) = [:X1, X2:] by FUNCT_3:def 3;

      then

      reconsider CAB = ( chi ( [:A, B:], [:X1, X2:])) as Function of [:X1, X2:], ExtREAL by T1, FUNCT_2: 2;

      

       QQ: for x be Element of X1 holds ((M2 . B) * (( chi (A,X1)) . x)) = ( Integral (M2,( ProjMap1 (CAB,x))))

      proof

        let x be Element of X1;

        

         QQ1: for y be Element of X2 holds (( ProjMap1 (CAB,x)) . y) = ((( chi (A,X1)) . x) * (( chi (B,X2)) . y))

        proof

          let y be Element of X2;

          (( ProjMap1 (CAB,x)) . y) = (( chi (( Union K), [:X1, X2:])) . (x,y)) by A2, MESFUNC9:def 6;

          hence thesis by A2, Th26;

        end;

        per cases ;

          suppose x in A;

          then

           QQ2: (( chi (A,X1)) . x) = 1 by FUNCT_3:def 3;

          then

           QQ4: ((M2 . B) * (( chi (A,X1)) . x)) = (M2 . B) by XXREAL_3: 81;

          

           QQ3: ( dom ( ProjMap1 (CAB,x))) = X2 by FUNCT_2:def 1

          .= ( dom ( chi (B,X2))) by FUNCT_3:def 3;

          for y be Element of X2 st y in ( dom ( ProjMap1 (CAB,x))) holds (( ProjMap1 (CAB,x)) . y) = (( chi (B,X2)) . y)

          proof

            let y be Element of X2;

            assume y in ( dom ( ProjMap1 (CAB,x)));

            (( ProjMap1 (CAB,x)) . y) = ((( chi (A,X1)) . x) * (( chi (B,X2)) . y)) by QQ1;

            hence (( ProjMap1 (CAB,x)) . y) = (( chi (B,X2)) . y) by QQ2, XXREAL_3: 81;

          end;

          then ( ProjMap1 (CAB,x)) = ( chi (B,X2)) by QQ3, PARTFUN1: 5;

          hence ((M2 . B) * (( chi (A,X1)) . x)) = ( Integral (M2,( ProjMap1 (CAB,x)))) by QQ4, MESFUNC9: 14;

        end;

          suppose not x in A;

          then

           QQ5: (( chi (A,X1)) . x) = 0 by FUNCT_3:def 3;

          then

           QQ9: ((M2 . B) * (( chi (A,X1)) . x)) = 0 ;

          

           QQ8: {} is Element of S2 by PROB_1: 4;

          

           QQ6: ( dom ( ProjMap1 (CAB,x))) = X2 by FUNCT_2:def 1

          .= ( dom ( chi ( {} ,X2))) by FUNCT_3:def 3;

          for y be Element of X2 st y in ( dom ( ProjMap1 (CAB,x))) holds (( ProjMap1 (CAB,x)) . y) = (( chi ( {} ,X2)) . y)

          proof

            let y be Element of X2;

            assume y in ( dom ( ProjMap1 (CAB,x)));

            (( ProjMap1 (CAB,x)) . y) = ((( chi (A,X1)) . x) * (( chi (B,X2)) . y)) by QQ1;

            then (( ProjMap1 (CAB,x)) . y) = 0 by QQ5;

            hence (( ProjMap1 (CAB,x)) . y) = (( chi ( {} ,X2)) . y) by FUNCT_3:def 3;

          end;

          then ( ProjMap1 (CAB,x)) = ( chi ( {} ,X2)) by QQ6, PARTFUN1: 5;

          then ( Integral (M2,( ProjMap1 (CAB,x)))) = (M2 . {} ) by QQ8, MESFUNC9: 14;

          hence ((M2 . B) * (( chi (A,X1)) . x)) = ( Integral (M2,( ProjMap1 (CAB,x)))) by QQ9, VALUED_0:def 19;

        end;

      end;

      

       RB1: ( dom XD) = NAT by FUNCT_2:def 1;

      for n be object st n in NAT holds (XD . n) in ( Funcs (X1, REAL ))

      proof

        let n be object;

        assume n in NAT ;

        then

        reconsider n1 = n as Element of NAT ;

        

         RB2: (XD . n) = ( chi ((D . n1),X1)) by B5;

        then

         RB3: ( dom (XD . n)) = X1 by FUNCT_3:def 3;

        ( rng (XD . n)) c= { 0 , 1} & { 0 , 1} c= REAL by RB2, FUNCT_3: 39, XREAL_0:def 1;

        then ( rng (XD . n)) c= REAL ;

        hence (XD . n) in ( Funcs (X1, REAL )) by RB3, FUNCT_2:def 2;

      end;

      then

      reconsider RXD = XD as sequence of ( Funcs (X1, REAL )) by RB1, FUNCT_2: 3;

      

       Y3: for n be Nat holds (D . n) c= A & (E . n) c= B

      proof

        let n be Nat;

        n is Element of NAT by ORDINAL1:def 12;

        then

         YY1: (D . n) = ( proj1 (K . n)) & (E . n) = ( proj2 (K . n)) by B4, C4;

        ( proj1 (K . n)) c= ( proj1 ( Union K)) & ( proj1 ( Union K)) c= A & ( proj2 (K . n)) c= ( proj2 ( Union K)) & ( proj2 ( Union K)) c= B by A2, XTUPLE_0: 8, XTUPLE_0: 9, FUNCT_5: 10, ABCMIZ_1: 1;

        hence (D . n) c= A & (E . n) c= B by YY1;

      end;

      

       Z1: for x be Element of X1 holds ex XF be Functional_Sequence of X2, ExtREAL , I be ExtREAL_sequence st (for n be Nat holds (XF . n) = (((RXD . n) . x) (#) ( chi ((E . n),X2)))) & (for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x))) & I is summable & ( Integral (M2,( lim ( Partial_Sums XF)))) = ( Sum I)

      proof

        let x be Element of X1;

        deffunc FF( Nat) = (((RXD . $1) . x) (#) ( chi ((E . $1),X2)));

        defpred FP[ Nat, object] means $2 = FF($1);

        

         W1: for n be Element of NAT holds ex y be Element of ( PFuncs (X2, ExtREAL )) st FP[n, y]

        proof

          let n be Element of NAT ;

          reconsider r = ((RXD . n) . x) as Real;

          reconsider y = FF(n) as Element of ( PFuncs (X2, ExtREAL )) by PARTFUN1: 45;

          take y;

          thus FP[n, y];

        end;

        consider XF be Function of NAT , ( PFuncs (X2, ExtREAL )) such that

         W2: for n be Element of NAT holds FP[n, (XF . n)] from FUNCT_2:sch 3( W1);

        reconsider XF as Functional_Sequence of X2, ExtREAL ;

        

         Y2: for n be Nat holds (XF . n) = (((RXD . n) . x) (#) ( chi ((E . n),X2)))

        proof

          let n be Nat;

          n is Element of NAT by ORDINAL1:def 12;

          hence thesis by W2;

        end;

        consider I be ExtREAL_sequence such that

         Y4: (for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x))) & I is summable & ( Integral (M2,( lim ( Partial_Sums XF)))) = ( Sum I) by B5, Y2, Y3, Th30;

        thus ex XF be Functional_Sequence of X2, ExtREAL , I be ExtREAL_sequence st (for n be Nat holds (XF . n) = (((RXD . n) . x) (#) ( chi ((E . n),X2)))) & (for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x))) & I is summable & ( Integral (M2,( lim ( Partial_Sums XF)))) = ( Sum I) by Y2, Y4;

      end;

      ( dom ( lim ( Partial_Sums XK))) = ( dom (( Partial_Sums XK) . 0 )) by MESFUNC8:def 9;

      then ( dom ( lim ( Partial_Sums XK))) = ( dom (XK . 0 )) by MESFUNC9:def 4;

      then ( dom ( lim ( Partial_Sums XK))) = ( dom ( chi ((K . 0 ), [:X1, X2:]))) by A3;

      then

       QR0: ( dom ( lim ( Partial_Sums XK))) = [:X1, X2:] by FUNCT_3:def 3;

      then

      reconsider LPSXK = ( lim ( Partial_Sums XK)) as Function of [:X1, X2:], ExtREAL by FUNCT_2: 67;

      

       QR: for x be Element of X1, y be Element of X2 holds (( ProjMap1 (CAB,x)) . y) = (( ProjMap1 (LPSXK,x)) . y)

      proof

        let x be Element of X1, y be Element of X2;

        

         QR1: [x, y] in [:X1, X2:] by ZFMISC_1:def 2;

        (( ProjMap1 (CAB,x)) . y) = (( chi ( [:A, B:], [:X1, X2:])) . (x,y)) by MESFUNC9:def 6

        .= (LPSXK . (x,y)) by A3, Th25, QR1, A2;

        hence (( ProjMap1 (CAB,x)) . y) = (( ProjMap1 (LPSXK,x)) . y) by MESFUNC9:def 6;

      end;

      

       QS: for x be Element of X1 holds ( ProjMap1 (CAB,x)) = ( ProjMap1 (LPSXK,x))

      proof

        let x be Element of X1;

        for y be Element of X2 holds (( ProjMap1 (CAB,x)) . y) = (( ProjMap1 (LPSXK,x)) . y) by QR;

        hence thesis by FUNCT_2:def 8;

      end;

      

       QT: for x be Element of X1 holds ((M2 . B) * (( chi (A,X1)) . x)) = ( Integral (M2,( ProjMap1 (LPSXK,x))))

      proof

        let x be Element of X1;

        ( ProjMap1 (CAB,x)) = ( ProjMap1 (LPSXK,x)) by QS;

        hence thesis by QQ;

      end;

      

       ZZ: for x be Element of X1 holds ex I be ExtREAL_sequence st (for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x))) & ((M2 . B) * (( chi (A,X1)) . x)) = ( Sum I)

      proof

        let x be Element of X1;

        consider XF be Functional_Sequence of X2, ExtREAL , I be ExtREAL_sequence such that

         Z3: (for n be Nat holds (XF . n) = (((RXD . n) . x) (#) ( chi ((E . n),X2)))) & (for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x))) & I is summable & ( Integral (M2,( lim ( Partial_Sums XF)))) = ( Sum I) by Z1;

        ( dom ( lim ( Partial_Sums XF))) = ( dom (( Partial_Sums XF) . 0 )) by MESFUNC8:def 9;

        then

         Z31: ( dom ( lim ( Partial_Sums XF))) = ( dom (XF . 0 )) by MESFUNC9:def 4;

        then ( dom ( lim ( Partial_Sums XF))) = ( dom (((RXD . 0 ) . x) (#) ( chi ((E . 0 ),X2)))) by Z3;

        then ( dom ( lim ( Partial_Sums XF))) = ( dom ( chi ((E . 0 ),X2))) by MESFUNC1:def 6;

        then

         Z4A: ( dom ( lim ( Partial_Sums XF))) = X2 by FUNCT_3:def 3;

        then

         Z4: ( dom ( ProjMap1 (LPSXK,x))) = ( dom ( lim ( Partial_Sums XF))) by FUNCT_2:def 1;

        now

          let y be Element of X2;

          assume

           Z41: y in ( dom ( ProjMap1 (LPSXK,x)));

          

           Z42: (( ProjMap1 (LPSXK,x)) . y) = (LPSXK . (x,y)) by MESFUNC9:def 6;

          reconsider z = [x, y] as Element of [:X1, X2:] by ZFMISC_1:def 2;

          

           Z46: for n be Nat holds ( dom (XK . n)) = [:X1, X2:]

          proof

            let n be Nat;

            (XK . n) = ( chi ((K . n), [:X1, X2:])) by A3;

            hence ( dom (XK . n)) = [:X1, X2:] by FUNCT_3:def 3;

          end;

          

           Z49: for n be Nat holds (XK . n) is nonnegative

          proof

            let n be Nat;

            for z be object holds 0 <= ((XK . n) . z)

            proof

              let z be object;

              

               Z45: (XK . n) = ( chi ((K . n), [:X1, X2:])) by A3;

              

               Z44: ( dom (XK . n)) = [:X1, X2:] by Z46;

              per cases ;

                suppose not z in [:X1, X2:];

                hence ((XK . n) . z) >= 0 by Z44, FUNCT_1:def 2;

              end;

                suppose z in [:X1, X2:] & z in (K . n);

                hence ((XK . n) . z) >= 0 by Z45, FUNCT_3:def 3;

              end;

                suppose z in [:X1, X2:] & not z in (K . n);

                hence ((XK . n) . z) >= 0 by Z45, FUNCT_3:def 3;

              end;

            end;

            hence (XK . n) is nonnegative by SUPINF_2: 51;

          end;

          for n,m be Nat holds ( dom (XK . n)) = ( dom (XK . m))

          proof

            let n,m be Nat;

            ( dom (XK . n)) = [:X1, X2:] by Z46;

            hence ( dom (XK . n)) = ( dom (XK . m)) by Z46;

          end;

          then

           Z48: XK is with_the_same_dom by MESFUNC8:def 2;

          

           ZZ1: ( dom (XK . 0 )) = [:X1, X2:] by Z46;

          then

           ZP1: (( Partial_Sums XK) # z) is convergent by Z49, Z48, MESFUNC9: 38;

          

           Z50: for n be Nat holds ( dom (XF . n)) = X2

          proof

            let n be Nat;

            (XF . n) = (((RXD . n) . x) (#) ( chi ((E . n),X2))) by Z3;

            then ( dom (XF . n)) = ( dom ( chi ((E . n),X2))) by MESFUNC1:def 6;

            hence ( dom (XF . n)) = X2 by FUNCT_3:def 3;

          end;

          

           ZZ5: for n,m be Nat holds ( dom (XF . n)) = ( dom (XF . m))

          proof

            let n,m be Nat;

            ( dom (XF . n)) = X2 by Z50;

            hence ( dom (XF . n)) = ( dom (XF . m)) by Z50;

          end;

          then

           Z51: XF is with_the_same_dom by MESFUNC8:def 2;

          

           ZX1: for n be Nat holds (XF . n) is nonnegative

          proof

            let n be Nat;

            for y be object holds 0 <= ((XF . n) . y)

            proof

              let y be object;

              

               Z53: (XF . n) = (((RXD . n) . x) (#) ( chi ((E . n),X2))) by Z3;

              

               Z54: ( dom (XF . n)) = X2 by Z50;

              per cases ;

                suppose not y in X2;

                hence ((XF . n) . y) >= 0 by Z54, FUNCT_1:def 2;

              end;

                suppose

                 Z55: y in X2 & y in (E . n);

                then

                reconsider y1 = y as Element of X2;

                

                 Z56: ((XF . n) . y) = (((RXD . n) . x) * (( chi ((E . n),X2)) . y1)) by Z53, Z54, MESFUNC1:def 6;

                (( chi ((E . n),X2)) . y1) = 1 by Z55, FUNCT_3:def 3;

                then ((XF . n) . y) = ((RXD . n) . x) by Z56, XXREAL_3: 81;

                then ((XF . n) . y) = (( chi ((D . n),X1)) . x) by B5;

                hence ((XF . n) . y) >= 0 by SUPINF_2: 51;

              end;

                suppose

                 Z57: y in X2 & not y in (E . n);

                then

                reconsider y1 = y as Element of X2;

                

                 Z58: ((XF . n) . y) = (((RXD . n) . x) * (( chi ((E . n),X2)) . y1)) by Z53, Z54, MESFUNC1:def 6;

                (( chi ((E . n),X2)) . y1) = 0 by Z57, FUNCT_3:def 3;

                hence ((XF . n) . y) >= 0 by Z58;

              end;

            end;

            hence (XF . n) is nonnegative by SUPINF_2: 51;

          end;

          then

           ZP2: (( Partial_Sums XF) # y) is convergent by Z51, Z31, Z4A, MESFUNC9: 38;

          

           X20: for n be Nat holds ((( Partial_Sums XK) # z) . n) = ((( Partial_Sums XF) # y) . n)

          proof

            let n be Nat;

            

             X17: ((( Partial_Sums XK) # z) . n) = ((( Partial_Sums XK) . n) . z) & ((( Partial_Sums XF) # y) . n) = ((( Partial_Sums XF) . n) . y) by MESFUNC5:def 13;

            defpred P1[ Nat] means ((( Partial_Sums XK) . $1) . z) = ((( Partial_Sums XF) . $1) . y);

            ((( Partial_Sums XK) . 0 ) . z) = ((XK . 0 ) . (x,y)) by MESFUNC9:def 4;

            then

             X14: ((( Partial_Sums XK) . 0 ) . z) = (((XD . 0 ) . x) * ((XE . 0 ) . y)) by E0;

            

             X13: y in ( dom (((RXD . 0 ) . x) (#) ( chi ((E . 0 ),X2)))) by Z3, Z31, Z4, Z41;

            (( Partial_Sums XF) . 0 ) = (XF . 0 ) by MESFUNC9:def 4;

            then ((( Partial_Sums XF) . 0 ) . y) = ((((RXD . 0 ) . x) (#) ( chi ((E . 0 ),X2))) . y) by Z3;

            then ((( Partial_Sums XF) . 0 ) . y) = (((XD . 0 ) . x) * (( chi ((E . 0 ),X2)) . y)) by X13, MESFUNC1:def 6;

            then

             X15: P1[ 0 ] by C5, X14;

            

             X16: for n be Nat st P1[n] holds P1[(n + 1)]

            proof

              let n be Nat;

              assume

               X18: P1[n];

              

               X30: ( dom (( Partial_Sums XK) . (n + 1))) = ( dom (XK . 0 )) by Z49, Z48, MESFUNC9: 29, MESFUNC9: 30;

              (( Partial_Sums XK) . (n + 1)) = ((( Partial_Sums XK) . n) + (XK . (n + 1))) by MESFUNC9:def 4;

              then

               X31: ((( Partial_Sums XK) . (n + 1)) . z) = (((( Partial_Sums XK) . n) . z) + ((XK . (n + 1)) . z)) by ZZ1, X30, MESFUNC1:def 3;

              

               X32: ( dom (( Partial_Sums XF) . (n + 1))) = ( dom (XF . 0 )) by Z51, ZX1, MESFUNC9: 30, MESFUNC9: 29;

              (( Partial_Sums XF) . (n + 1)) = ((( Partial_Sums XF) . n) + (XF . (n + 1))) by MESFUNC9:def 4;

              then

               X33: ((( Partial_Sums XF) . (n + 1)) . y) = (((( Partial_Sums XF) . n) . y) + ((XF . (n + 1)) . y)) by Z31, Z4A, X32, MESFUNC1:def 3;

              ((XK . (n + 1)) . z) = ((XK . (n + 1)) . (x,y));

              then

               X35: ((XK . (n + 1)) . z) = (((XD . (n + 1)) . x) * ((XE . (n + 1)) . y)) by E0;

              ( dom (XF . (n + 1))) = ( dom (XF . 0 )) by ZZ5;

              then

               X34: y in ( dom (((RXD . (n + 1)) . x) (#) ( chi ((E . (n + 1)),X2)))) by Z3, Z31, Z4, Z41;

              ((XF . (n + 1)) . y) = ((((RXD . (n + 1)) . x) (#) ( chi ((E . (n + 1)),X2))) . y) by Z3;

              then ((XF . (n + 1)) . y) = (((RXD . (n + 1)) . x) * (( chi ((E . (n + 1)),X2)) . y)) by X34, MESFUNC1:def 6;

              hence P1[(n + 1)] by C5, X35, X33, X31, X18;

            end;

            for n be Nat holds P1[n] from NAT_1:sch 2( X15, X16);

            hence ((( Partial_Sums XK) # z) . n) = ((( Partial_Sums XF) # y) . n) by X17;

          end;

          for n be Nat holds ((( Partial_Sums XK) # z) . n) <= ((( Partial_Sums XF) # y) . n) by X20;

          then

           ZP3: ( lim (( Partial_Sums XK) # z)) <= ( lim (( Partial_Sums XF) # y)) by ZP1, ZP2, RINFSUP2: 38;

          for n be Nat holds ((( Partial_Sums XF) # y) . n) <= ((( Partial_Sums XK) # z) . n) by X20;

          then ( lim (( Partial_Sums XF) # y)) <= ( lim (( Partial_Sums XK) # z)) by ZP1, ZP2, RINFSUP2: 38;

          then ( lim (( Partial_Sums XK) # z)) = ( lim (( Partial_Sums XF) # y)) by ZP3, XXREAL_0: 1;

          then (( lim ( Partial_Sums XK)) . z) = ( lim (( Partial_Sums XF) # y)) by QR0, MESFUNC8:def 9;

          hence (( ProjMap1 (LPSXK,x)) . y) = (( lim ( Partial_Sums XF)) . y) by Z42, Z4A, MESFUNC8:def 9;

        end;

        then ( ProjMap1 (LPSXK,x)) = ( lim ( Partial_Sums XF)) by Z4, PARTFUN1: 5;

        hence thesis by Z3, QT;

      end;

      defpred PI[ Nat, object] means ((M2 . (E . $1)) = +infty implies $2 = ( Xchi ((D . $1),X1))) & ((M2 . (E . $1)) <> +infty implies ex m2 be Real st m2 = (M2 . (E . $1)) & $2 = (m2 (#) ( chi ((D . $1),X1))));

      

       H1: for n be Element of NAT holds ex y be Element of ( PFuncs (X1, ExtREAL )) st PI[n, y]

      proof

        let n be Element of NAT ;

        per cases ;

          suppose

           HA1: (M2 . (E . n)) = +infty ;

          set y = ( Xchi ((D . n),X1));

          reconsider y as Element of ( PFuncs (X1, ExtREAL )) by PARTFUN1: 45;

           PI[n, y] by HA1;

          hence ex y be Element of ( PFuncs (X1, ExtREAL )) st PI[n, y];

        end;

          suppose

           HA2: (M2 . (E . n)) <> +infty ;

          (M2 . (E . n)) >= 0 by SUPINF_2: 51;

          then (M2 . (E . n)) in REAL by HA2, XXREAL_0: 14;

          then

          reconsider m2 = (M2 . (E . n)) as Real;

          set y = (m2 (#) ( chi ((D . n),X1)));

          reconsider y as Element of ( PFuncs (X1, ExtREAL )) by PARTFUN1: 45;

           PI[n, y];

          hence ex y be Element of ( PFuncs (X1, ExtREAL )) st PI[n, y];

        end;

      end;

      consider FI be Function of NAT , ( PFuncs (X1, ExtREAL )) such that

       H2: for n be Element of NAT holds PI[n, (FI . n)] from FUNCT_2:sch 3( H1);

      

       H3: for n be Nat holds ( dom (FI . n)) = X1

      proof

        let n be Nat;

        

         HA3: n is Element of NAT by ORDINAL1:def 12;

        per cases ;

          suppose (M2 . (E . n)) = +infty ;

          then (FI . n) = ( Xchi ((D . n),X1)) by H2, HA3;

          hence ( dom (FI . n)) = X1 by FUNCT_2:def 1;

        end;

          suppose (M2 . (E . n)) <> +infty ;

          then

          consider m2 be Real such that

           HA4: m2 = (M2 . (E . n)) & (FI . n) = (m2 (#) ( chi ((D . n),X1))) by H2, HA3;

          ( dom (FI . n)) = ( dom ( chi ((D . n),X1))) by HA4, MESFUNC1:def 6;

          hence ( dom (FI . n)) = X1 by FUNCT_3:def 3;

        end;

      end;

      

       F1: A c= ( dom (FI . 0 )) by H3, A10;

      

       F2A: for n be Nat holds (FI . n) is nonnegative

      proof

        let n be Nat;

        

         HA5: n is Element of NAT by ORDINAL1:def 12;

        per cases ;

          suppose (M2 . (E . n)) = +infty ;

          then (FI . n) = ( Xchi ((D . n),X1)) by H2, HA5;

          hence (FI . n) is nonnegative;

        end;

          suppose (M2 . (E . n)) <> +infty ;

          then

          consider m2 be Real such that

           HA6: m2 = (M2 . (E . n)) & (FI . n) = (m2 (#) ( chi ((D . n),X1))) by H2, HA5;

          for x be object holds ((FI . n) . x) >= 0

          proof

            let x be object;

            per cases ;

              suppose

               HA7: x in X1;

              then

              reconsider x1 = x as Element of X1;

              x1 in ( dom ( chi ((D . n),X1))) by HA7, FUNCT_3:def 3;

              then x1 in ( dom (FI . n)) by HA6, MESFUNC1:def 6;

              then

               HA8: ((FI . n) . x) = (m2 * (( chi ((D . n),X1)) . x1)) by HA6, MESFUNC1:def 6;

              m2 >= 0 & (( chi ((D . n),X1)) . x1) >= 0 by HA6, SUPINF_2: 51;

              hence ((FI . n) . x) >= 0 by HA8;

            end;

              suppose not x in X1;

              then not x in ( dom (FI . n));

              hence ((FI . n) . x) >= 0 by FUNCT_1:def 2;

            end;

          end;

          hence (FI . n) is nonnegative by SUPINF_2: 51;

        end;

      end;

      for n,m be Nat holds ( dom (FI . n)) = ( dom (FI . m))

      proof

        let n,m be Nat;

        ( dom (FI . n)) = X1 & ( dom (FI . m)) = X1 by H3;

        hence ( dom (FI . n)) = ( dom (FI . m));

      end;

      then

       F3: FI is with_the_same_dom by MESFUNC8:def 2;

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

      

       F4: for n be Nat holds (FI . n) is nonnegative & (FI . n) is A -measurable & (FI . n) is XX -measurable

      proof

        let n be Nat;

        

         F4A: n is Element of NAT by ORDINAL1:def 12;

        thus (FI . n) is nonnegative by F2A;

        per cases ;

          suppose (M2 . (E . n)) = +infty ;

          then (FI . n) = ( Xchi ((D . n),X1)) by H2, F4A;

          hence (FI . n) is A -measurable & (FI . n) is XX -measurable by Th32;

        end;

          suppose (M2 . (E . n)) <> +infty ;

          then

          consider m2 be Real such that

           F4B: m2 = (M2 . (E . n)) & (FI . n) = (m2 (#) ( chi ((D . n),X1))) by H2, F4A;

          ( dom ( chi ((D . n),X1))) = X1 by FUNCT_3:def 3;

          hence (FI . n) is A -measurable & (FI . n) is XX -measurable by F4B, MESFUNC2: 29, MESFUNC1: 37;

        end;

      end;

      

       F5: for x be Element of X1 st x in A holds (FI # x) is summable

      proof

        let x be Element of X1;

        assume x in A;

        for n be Element of NAT holds ((FI # x) . n) >= 0

        proof

          let n be Element of NAT ;

          ((FI # x) . n) = ((FI . n) . x) by MESFUNC5:def 13;

          hence ((FI # x) . n) >= 0 by F4, SUPINF_2: 51;

        end;

        then (FI # x) is nonnegative by SUPINF_2: 39;

        hence (FI # x) is summable by MEASURE8: 2;

      end;

      consider J be ExtREAL_sequence such that

       F6: (for n be Nat holds (J . n) = ( Integral (M1,((FI . n) | A)))) & J is summable & ( Integral (M1,(( lim ( Partial_Sums FI)) | A))) = ( Sum J) by F1, F3, F4, F5, MESFUNC9: 30, MESFUNC9: 51;

      

       G1: for n be Nat holds (J . n) = ( Integral (M1,(FI . n)))

      proof

        let n be Nat;

        

         F4A: n is Element of NAT by ORDINAL1:def 12;

        

         FF: XX = ( dom (FI . n)) by H3;

        

         T1: ex E be Element of S1 st E = ( dom (FI . n)) & (FI . n) is E -measurable

        proof

          take XX;

          thus thesis by FF, F4;

        end;

        for x be object st x in (( dom (FI . n)) \ A) holds ((FI . n) . x) = 0

        proof

          let x be object;

          assume

           T3: x in (( dom (FI . n)) \ A);

          then

           T3A: x in ( dom (FI . n)) & not x in A by XBOOLE_0:def 5;

          (D . n) c= A by Y3;

          then

           T6: not x in (D . n) by T3, XBOOLE_0:def 5;

          per cases ;

            suppose (M2 . (E . n)) = +infty ;

            then (FI . n) = ( Xchi ((D . n),X1)) by H2, F4A;

            hence ((FI . n) . x) = 0 by T6, T3, DefXchi;

          end;

            suppose (M2 . (E . n)) <> +infty ;

            then

            consider m2 be Real such that

             F4B: m2 = (M2 . (E . n)) & (FI . n) = (m2 (#) ( chi ((D . n),X1))) by H2, F4A;

            

             T5: ((FI . n) . x) = (m2 * (( chi ((D . n),X1)) . x)) by F4B, T3A, MESFUNC1:def 6;

            (( chi ((D . n),X1)) . x) = 0 by T3, T6, FUNCT_3:def 3;

            hence ((FI . n) . x) = 0 by T5;

          end;

        end;

        then ( Integral (M1,(FI . n))) = ( Integral (M1,((FI . n) | A))) by F4, T1, Th28;

        hence (J . n) = ( Integral (M1,(FI . n))) by F6;

      end;

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

      for n be Element of NAT holds (J . n) = ((( product-pre-Measure (M1,M2)) * K) . n)

      proof

        let n be Element of NAT ;

        ( Integral (M1,(FI . n))) = ((M2 . (E . n)) * (M1 . (D . n)))

        proof

          

           M2: XX = ( dom (FI . n)) by H3;

          

           M3b: (FI . n) is nonnegative by F4;

          per cases ;

            suppose

             M0: (M2 . (E . n)) = +infty ;

            then

             M1: (FI . n) = ( Xchi ((D . n),X1)) by H2;

            per cases ;

              suppose

               M5: (M1 . (D . n)) = 0 ;

              then ( Integral (M1,(FI . n))) = 0 by M1, Th34;

              hence ( Integral (M1,(FI . n))) = ((M2 . (E . n)) * (M1 . (D . n))) by M5;

            end;

              suppose

               Q1: (M1 . (D . n)) <> 0 ;

              then (M1 . (D . n)) > 0 by SUPINF_2: 51;

              then ((M2 . (E . n)) * (M1 . (D . n))) = +infty by M0, XXREAL_3:def 5;

              hence ( Integral (M1,(FI . n))) = ((M2 . (E . n)) * (M1 . (D . n))) by M1, Q1, Th34;

            end;

          end;

            suppose (M2 . (E . n)) <> +infty ;

            then

            consider m2 be Real such that

             R2: m2 = (M2 . (E . n)) & (FI . n) = (m2 (#) ( chi ((D . n),X1))) by H2;

            

             R3: m2 >= 0 by R2, SUPINF_2: 51;

            

             R4: XX = ( dom ( chi ((D . n),X1))) by FUNCT_3:def 3;

            

             R5: ( chi ((D . n),X1)) is XX -measurable by MESFUNC2: 29;

            ( integral+ (M1,(m2 (#) ( chi ((D . n),X1))))) = (m2 * ( integral+ (M1,( chi ((D . n),X1))))) by R4, MESFUNC2: 29, R3, MESFUNC5: 86;

            then ( integral+ (M1,(m2 (#) ( chi ((D . n),X1))))) = (m2 * ( Integral (M1,( chi ((D . n),X1))))) by R4, MESFUNC2: 29, MESFUNC5: 88;

            then ( integral+ (M1,(m2 (#) ( chi ((D . n),X1))))) = (m2 * (M1 . (D . n))) by MESFUNC9: 14;

            hence ( Integral (M1,(FI . n))) = ((M2 . (E . n)) * (M1 . (D . n))) by R2, M2, R4, R5, MESFUNC1: 37, M3b, MESFUNC5: 88;

          end;

        end;

        then

         Q9: (J . n) = ((M2 . (E . n)) * (M1 . (D . n))) by G1;

        

         Q17: ( dom K) = NAT by FUNCT_2:def 1;

        consider Dn be Element of S1, En be Element of S2 such that

         Q10: (K . n) = [:Dn, En:] & (( product-pre-Measure (M1,M2)) . (K . n)) = ((M1 . Dn) * (M2 . En)) by Def6;

        

         Q13: (D . n) = ( proj1 (K . n)) & (E . n) = ( proj2 (K . n)) by B4, C4;

        ((M1 . Dn) * (M2 . En)) = ((M1 . (D . n)) * (M2 . (E . n)))

        proof

          per cases ;

            suppose

             Q14: Dn = {} or En = {} ;

            then (M1 . Dn) = 0 or (M2 . En) = 0 by VALUED_0:def 19;

            then

             Q15: ((M1 . Dn) * (M2 . En)) = 0 ;

            (D . n) = {} & (E . n) = {} by Q13, Q10, Q14;

            then (M1 . (D . n)) = 0 & (M2 . (E . n)) = 0 by VALUED_0:def 19;

            hence ((M1 . Dn) * (M2 . En)) = ((M1 . (D . n)) * (M2 . (E . n))) by Q15;

          end;

            suppose Dn <> {} & En <> {} ;

            then Dn = (D . n) & En = (E . n) by Q10, Q13, FUNCT_5: 9;

            hence ((M1 . Dn) * (M2 . En)) = ((M1 . (D . n)) * (M2 . (E . n)));

          end;

        end;

        hence (J . n) = ((( product-pre-Measure (M1,M2)) * K) . n) by Q9, Q17, Q10, FUNCT_1: 13;

      end;

      then

       F7: J = (( product-pre-Measure (M1,M2)) * K) by FUNCT_2:def 8;

      

       V5: ( dom ( lim ( Partial_Sums FI))) = ( dom (( Partial_Sums FI) . 0 )) by MESFUNC8:def 9;

      then

       V0: ( dom ( lim ( Partial_Sums FI))) = ( dom (FI . 0 )) by MESFUNC9:def 4;

      then

       V1: XX = ( dom ( lim ( Partial_Sums FI))) by H3;

      for x be Element of X1 holds (( lim ( Partial_Sums FI)) . x) >= 0

      proof

        let x be Element of X1;

        (( Partial_Sums FI) # x) is non-decreasing by V0, V1, F3, F2A, MESFUNC9: 38;

        then ( lim (( Partial_Sums FI) # x)) = ( sup (( Partial_Sums FI) # x)) by RINFSUP2: 37;

        then ((( Partial_Sums FI) # x) . 0 ) <= ( lim (( Partial_Sums FI) # x)) by RINFSUP2: 23;

        then ((( Partial_Sums FI) . 0 ) . x) <= ( lim (( Partial_Sums FI) # x)) by MESFUNC5:def 13;

        then ((FI . 0 ) . x) <= ( lim (( Partial_Sums FI) # x)) by MESFUNC9:def 4;

        then 0 <= ( lim (( Partial_Sums FI) # x)) by F2A, SUPINF_2: 51;

        hence 0 <= (( lim ( Partial_Sums FI)) . x) by V1, MESFUNC8:def 9;

      end;

      then

       V4: ( lim ( Partial_Sums FI)) is nonnegative by SUPINF_2: 39;

      

       W4: ( Partial_Sums FI) is with_the_same_dom by F2A, F3, MESFUNC9: 30, MESFUNC9: 43;

      for n be Nat holds (FI . n) is XX -measurable & (FI . n) is without-infty

      proof

        let n be Nat;

        thus (FI . n) is XX -measurable by F4;

        (FI . n) is nonnegative by F4;

        hence (FI . n) is without-infty;

      end;

      then

       W1: for n be Nat holds (( Partial_Sums FI) . n) is XX -measurable by MESFUNC9: 41;

      

       V2: for x be Element of X1 st x in XX holds (( Partial_Sums FI) # x) is convergent by V0, V1, F3, F2A, MESFUNC9: 38;

      

       V3: for x be object st x in (( dom ( lim ( Partial_Sums FI))) \ A) holds (( lim ( Partial_Sums FI)) . x) = 0

      proof

        let x be object;

        assume

         VV1: x in (( dom ( lim ( Partial_Sums FI))) \ A);

        then

        reconsider x1 = x as Element of X1;

        for n be Nat holds ((( Partial_Sums FI) # x1) . n) = 0

        proof

          let n be Nat;

          

           VV4: x1 in X1;

          then x1 in ( dom (FI . 0 )) by H3;

          then

           VV7: ((( Partial_Sums FI) # x1) . n) = (( Partial_Sums (FI # x1)) . n) by F2A, F3, MESFUNC9: 30, MESFUNC9: 32;

          

           VV8: for k be Nat holds ((FI # x1) . k) = 0

          proof

            let k be Nat;

            

             F4A: k is Element of NAT by ORDINAL1:def 12;

            (D . k) c= A by Y3;

            then

             VV2: not x1 in (D . k) by VV1, XBOOLE_0:def 5;

            per cases ;

              suppose (M2 . (E . k)) = +infty ;

              then (FI . k) = ( Xchi ((D . k),X1)) by H2, F4A;

              then ((FI . k) . x1) = 0 by VV2, DefXchi;

              hence ((FI # x1) . k) = 0 by MESFUNC5:def 13;

            end;

              suppose (M2 . (E . k)) <> +infty ;

              then

              consider m2 be Real such that

               VV3: m2 = (M2 . (E . k)) & (FI . k) = (m2 (#) ( chi ((D . k),X1))) by H2, F4A;

              

               VV5: (( chi ((D . k),X1)) . x1) = 0 by VV2, FUNCT_3:def 3;

              x1 in ( dom (FI . k)) by VV4, H3;

              then ((FI . k) . x1) = (m2 * (( chi ((D . k),X1)) . x1)) by VV3, MESFUNC1:def 6;

              hence ((FI # x1) . k) = 0 by VV5, MESFUNC5:def 13;

            end;

          end;

          defpred P[ Nat] means (( Partial_Sums (FI # x1)) . $1) = 0 ;

          (( Partial_Sums (FI # x1)) . 0 ) = ((FI # x1) . 0 ) by MESFUNC9:def 1;

          then

           VV9: P[ 0 ] by VV8;

          

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

          proof

            let k be Nat;

            assume

             VV11: P[k];

            (( Partial_Sums (FI # x1)) . (k + 1)) = ((( Partial_Sums (FI # x1)) . k) + ((FI # x1) . (k + 1))) by MESFUNC9:def 1

            .= ((( Partial_Sums (FI # x1)) . k) + 0 ) by VV8

            .= (( Partial_Sums (FI # x1)) . k) by XXREAL_3: 4;

            hence P[(k + 1)] by VV11;

          end;

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

          hence ((( Partial_Sums FI) # x1) . n) = 0 by VV7;

        end;

        then ( lim (( Partial_Sums FI) # x1)) = 0 by MESFUNC5: 52;

        hence (( lim ( Partial_Sums FI)) . x) = 0 by V1, MESFUNC8:def 9;

      end;

      

       F9: ( Integral (M1,( lim ( Partial_Sums FI)))) = ( Integral (M1,(( lim ( Partial_Sums FI)) | A))) by V1, V2, V3, V4, Th28, V5, W1, W4, MESFUNC8: 25;

      ( Integral (M1,( lim ( Partial_Sums FI)))) = ((M1 . A) * (M2 . B))

      proof

        

         J1: ( lim ( Partial_Sums FI)) is Function of X1, ExtREAL by V1, FUNCT_2:def 1;

        per cases ;

          suppose

           I0: (M2 . B) = +infty ;

          for x be Element of X1 holds (( lim ( Partial_Sums FI)) . x) = (( Xchi (A,X1)) . x)

          proof

            let x be Element of X1;

            

             JJ: x in X1;

            

             J2: ( dom (FI . 0 )) = X1 by H3;

            

             J4: (( lim ( Partial_Sums FI)) . x) = ( lim (( Partial_Sums FI) # x)) by V1, MESFUNC8:def 9;

            consider I be ExtREAL_sequence such that

             J5: for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x)) & ((M2 . B) * (( chi (A,X1)) . x)) = ( Sum I) by ZZ;

            

             J6: ( lim ( Partial_Sums I)) = ((M2 . B) * (( chi (A,X1)) . x)) by J5, MESFUNC9:def 3;

            for n be Element of NAT holds ((FI # x) . n) = (I . n)

            proof

              let n be Element of NAT ;

              per cases ;

                suppose

                 J8: (M2 . (E . n)) = +infty ;

                then (FI . n) = ( Xchi ((D . n),X1)) by H2;

                then

                 J9: ((FI # x) . n) = (( Xchi ((D . n),X1)) . x) by MESFUNC5:def 13;

                per cases ;

                  suppose

                   J10: x in (D . n);

                  then

                   J11: ((FI # x) . n) = +infty by J9, DefXchi;

                  (( chi ((D . n),X1)) . x) = 1 by J10, FUNCT_3:def 3;

                  then ((M2 . (E . n)) * (( chi ((D . n),X1)) . x)) = +infty by J8, XXREAL_3: 81;

                  hence ((FI # x) . n) = (I . n) by J5, J11;

                end;

                  suppose

                   J12: not x in (D . n);

                  then

                   J13: ((FI # x) . n) = 0 by J9, DefXchi;

                  (( chi ((D . n),X1)) . x) = 0 by J12, FUNCT_3:def 3;

                  then ((M2 . (E . n)) * (( chi ((D . n),X1)) . x)) = 0 ;

                  hence ((FI # x) . n) = (I . n) by J5, J13;

                end;

              end;

                suppose (M2 . (E . n)) <> +infty ;

                then

                consider m2 be Real such that

                 J15: m2 = (M2 . (E . n)) & (FI . n) = (m2 (#) ( chi ((D . n),X1))) by H2;

                x in ( dom (FI . n)) by JJ, H3;

                then ((FI . n) . x) = (m2 * (( chi ((D . n),X1)) . x)) by J15, MESFUNC1:def 6;

                then ((FI # x) . n) = (m2 * (( chi ((D . n),X1)) . x)) by MESFUNC5:def 13;

                hence ((FI # x) . n) = (I . n) by J15, J5;

              end;

            end;

            then (FI # x) = I by FUNCT_2: 63;

            then

             J17: for n be Element of NAT holds ((( Partial_Sums FI) # x) . n) = (( Partial_Sums I) . n) by F2A, F3, J2, MESFUNC9: 30, MESFUNC9: 32;

            (( Xchi (A,X1)) . x) = ((M2 . B) * (( chi (A,X1)) . x))

            proof

              per cases ;

                suppose

                 J18: x in A;

                then

                 J19: (( Xchi (A,X1)) . x) = +infty by DefXchi;

                (( chi (A,X1)) . x) = 1 by J18, FUNCT_3:def 3;

                hence (( Xchi (A,X1)) . x) = ((M2 . B) * (( chi (A,X1)) . x)) by J19, I0, XXREAL_3: 81;

              end;

                suppose

                 J20: not x in A;

                then

                 J21: (( Xchi (A,X1)) . x) = 0 by DefXchi;

                (( chi (A,X1)) . x) = 0 by J20, FUNCT_3:def 3;

                hence (( Xchi (A,X1)) . x) = ((M2 . B) * (( chi (A,X1)) . x)) by J21;

              end;

            end;

            hence (( lim ( Partial_Sums FI)) . x) = (( Xchi (A,X1)) . x) by J17, J4, J6, FUNCT_2: 63;

          end;

          then

           I1: ( lim ( Partial_Sums FI)) = ( Xchi (A,X1)) by J1, FUNCT_2: 63;

          per cases ;

            suppose

             I2: (M1 . A) <> 0 ;

            then (M1 . A) > 0 by SUPINF_2: 51;

            then ((M1 . A) * (M2 . B)) = +infty by I0, XXREAL_3:def 5;

            hence ( Integral (M1,( lim ( Partial_Sums FI)))) = ((M1 . A) * (M2 . B)) by I1, I2, Th34;

          end;

            suppose

             I3: (M1 . A) = 0 ;

            then ((M1 . A) * (M2 . B)) = 0 ;

            hence ( Integral (M1,( lim ( Partial_Sums FI)))) = ((M1 . A) * (M2 . B)) by I1, I3, Th34;

          end;

        end;

          suppose

           J22: (M2 . B) <> +infty ;

          (M2 . B) >= 0 by SUPINF_2: 51;

          then (M2 . B) in REAL by J22, XXREAL_0: 14;

          then

          reconsider M2B = (M2 . B) as Real;

          

           G3: X1 = ( dom ( chi (A,X1))) by FUNCT_3:def 3;

          ( dom (M2B (#) ( chi (A,X1)))) = ( dom ( chi (A,X1))) by MESFUNC1:def 6;

          then

           G0: ( dom (M2B (#) ( chi (A,X1)))) = X1 by FUNCT_3:def 3;

          then

           G1: (M2B (#) ( chi (A,X1))) is Function of X1, ExtREAL by FUNCT_2:def 1;

          

           R5: ( chi (A,X1)) is XX -measurable by MESFUNC2: 29;

          for x be Element of X1 holds (( lim ( Partial_Sums FI)) . x) = ((M2B (#) ( chi (A,X1))) . x)

          proof

            let x be Element of X1;

            

             JJ: x in X1;

            

             J2: ( dom (FI . 0 )) = X1 by H3;

            

             J4: (( lim ( Partial_Sums FI)) . x) = ( lim (( Partial_Sums FI) # x)) by V1, MESFUNC8:def 9;

            consider I be ExtREAL_sequence such that

             J5: for n be Nat holds (I . n) = ((M2 . (E . n)) * (( chi ((D . n),X1)) . x)) & ((M2 . B) * (( chi (A,X1)) . x)) = ( Sum I) by ZZ;

            

             J6: ( lim ( Partial_Sums I)) = ((M2 . B) * (( chi (A,X1)) . x)) by J5, MESFUNC9:def 3;

            for n be Element of NAT holds ((FI # x) . n) = (I . n)

            proof

              let n be Element of NAT ;

              (M2 . (E . n)) <= (M2 . B) & (M2 . B) < +infty by Y3, MEASURE1: 8, J22, XXREAL_0: 4;

              then

              consider m2 be Real such that

               J15: m2 = (M2 . (E . n)) & (FI . n) = (m2 (#) ( chi ((D . n),X1))) by H2;

              x in ( dom (FI . n)) by JJ, H3;

              then ((FI . n) . x) = (m2 * (( chi ((D . n),X1)) . x)) by J15, MESFUNC1:def 6;

              then ((FI # x) . n) = (m2 * (( chi ((D . n),X1)) . x)) by MESFUNC5:def 13;

              hence ((FI # x) . n) = (I . n) by J15, J5;

            end;

            then (FI # x) = I by FUNCT_2: 63;

            then for n be Element of NAT holds ((( Partial_Sums FI) # x) . n) = (( Partial_Sums I) . n) by F2A, F3, J2, MESFUNC9: 30, MESFUNC9: 32;

            then ( lim (( Partial_Sums FI) # x)) = ( lim ( Partial_Sums I)) by FUNCT_2: 63;

            hence (( lim ( Partial_Sums FI)) . x) = ((M2B (#) ( chi (A,X1))) . x) by J4, J6, G0, MESFUNC1:def 6;

          end;

          then ( lim ( Partial_Sums FI)) = (M2B (#) ( chi (A,X1))) by J1, G1, FUNCT_2: 63;

          then ( integral+ (M1,( lim ( Partial_Sums FI)))) = (M2B * ( integral+ (M1,( chi (A,X1))))) by SUPINF_2: 51, G3, R5, MESFUNC5: 86;

          then ( Integral (M1,( lim ( Partial_Sums FI)))) = (M2B * ( integral+ (M1,( chi (A,X1))))) by V1, V2, V4, V5, W1, W4, MESFUNC8: 25, MESFUNC5: 88;

          then ( Integral (M1,( lim ( Partial_Sums FI)))) = (M2B * ( Integral (M1,( chi (A,X1))))) by G3, R5, MESFUNC5: 88;

          hence ( Integral (M1,( lim ( Partial_Sums FI)))) = ((M1 . A) * (M2 . B)) by MESFUNC9: 14;

        end;

      end;

      hence thesis by F9, HH2, F6, F7, MEASURE8: 2;

    end;

    theorem :: MEASUR10:35

    

     Th36: for f be without-infty FinSequence of ExtREAL , s be without-infty ExtREAL_sequence st (for n be object st n in ( dom f) holds (f . n) = (s . n)) holds (( Sum f) + (s . 0 )) = (( Partial_Sums s) . ( len f))

    proof

      let f be without-infty FinSequence of ExtREAL , s be without-infty ExtREAL_sequence;

      assume

       A1: for n be object st n in ( dom f) holds (f . n) = (s . n);

      consider F be sequence of ExtREAL such that

       A2: ( Sum f) = (F . ( len f)) & (F . 0 ) = 0 & for i be Nat st i < ( len f) holds (F . (i + 1)) = ((F . i) + (f . (i + 1))) by EXTREAL1:def 2;

      defpred P[ Nat] means $1 <= ( len f) implies ((F . $1) + (s . 0 )) = (( Partial_Sums s) . $1) & (F . $1) <> -infty ;

      ((F . 0 ) + (s . 0 )) = (s . 0 ) by A2, XXREAL_3: 4;

      then

       a3: P[ 0 ] by A2, MESFUNC9:def 1;

      

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

      proof

        let k be Nat;

        assume

         a5: P[k];

        hereby

          assume

           a7: (k + 1) <= ( len f);

          then

           b0: (k + 1) in ( dom f) by NAT_1: 11, FINSEQ_3: 25;

          then

           a8: (f . (k + 1)) <> -infty by MESFUNC5: 10;

          ( dom s) = NAT by FUNCT_2:def 1;

          then

           a9: (s . 0 ) <> -infty by MESFUNC5: 10;

          

           d1: (F . (k + 1)) = ((F . k) + (f . (k + 1))) by A2, a7, NAT_1: 13;

          

          then ((F . (k + 1)) + (s . 0 )) = (((F . k) + (s . 0 )) + (f . (k + 1))) by a5, a7, NAT_1: 13, a8, a9, XXREAL_3: 29

          .= ((( Partial_Sums s) . k) + (s . (k + 1))) by b0, A1, a5, a7, NAT_1: 13;

          hence ((F . (k + 1)) + (s . 0 )) = (( Partial_Sums s) . (k + 1)) by MESFUNC9:def 1;

          thus (F . (k + 1)) <> -infty by d1, a5, a7, NAT_1: 13, a8, XXREAL_3: 17;

        end;

      end;

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

      hence (( Sum f) + (s . 0 )) = (( Partial_Sums s) . ( len f)) by A2;

    end;

    theorem :: MEASUR10:36

    

     Th37: for f be nonnegative FinSequence of ExtREAL , s be ExtREAL_sequence st (for n be object st n in ( dom f) holds (f . n) = (s . n)) & (for n be Element of NAT st not n in ( dom f) holds (s . n) = 0 ) holds ( Sum f) = ( Sum s) & ( Sum f) = ( SUM s)

    proof

      let f be nonnegative FinSequence of ExtREAL , s be ExtREAL_sequence;

      assume that

       a1: for n be object st n in ( dom f) holds (f . n) = (s . n) and

       a2: for n be Element of NAT st not n in ( dom f) holds (s . n) = 0 ;

      for n be object st n in ( dom s) holds 0 <= (s . n)

      proof

        let n be object;

        assume

         L1: n in ( dom s);

        per cases ;

          suppose n in ( dom f);

          then (f . n) = (s . n) by a1;

          hence 0 <= (s . n) by SUPINF_2: 51;

        end;

          suppose not n in ( dom f);

          hence 0 <= (s . n) by a2, L1;

        end;

      end;

      then

       a7: s is nonnegative by SUPINF_2: 52;

      then

       a5: (( Sum f) + (s . 0 )) = (( Partial_Sums s) . ( len f)) by a1, Th36;

       not 0 in ( dom f) by FINSEQ_3: 24;

      then (s . 0 ) = 0 by a2;

      then

       a6: ( Sum f) = (( Partial_Sums s) . ( len f)) by a5, XXREAL_3: 4;

      ( Partial_Sums s) is nonnegative & ( Partial_Sums s) is non-decreasing by a7, MESFUNC9: 16;

      then ( Partial_Sums s) is convergent by RINFSUP2: 37;

      then

       a9: (( Partial_Sums s) ^\ ( len f)) is convergent & ( lim ( Partial_Sums s)) = ( lim (( Partial_Sums s) ^\ ( len f))) by RINFSUP2: 21;

      defpred P[ Nat] means (( Partial_Sums s) . ( len f)) = ((( Partial_Sums s) ^\ ( len f)) . $1);

      (( Partial_Sums s) . ( len f)) = (( Partial_Sums s) . (( len f) + 0 ));

      then

       b1: P[ 0 ] by NAT_1:def 3;

      

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

      proof

        let k be Nat;

        assume

         b3: P[k];

        (( len f) + 0 ) < (( len f) + (k + 1)) by XREAL_1: 6;

        then not (( len f) + (k + 1)) in ( dom f) by FINSEQ_3: 25;

        then

         b4: (s . (( len f) + (k + 1))) = 0 by a2;

        ((( Partial_Sums s) ^\ ( len f)) . (k + 1)) = (( Partial_Sums s) . (( len f) + (k + 1))) by NAT_1:def 3

        .= ((( Partial_Sums s) . (( len f) + k)) + (s . ((( len f) + k) + 1))) by MESFUNC9:def 1

        .= (((( Partial_Sums s) ^\ ( len f)) . k) + 0 ) by b4, NAT_1:def 3;

        hence P[(k + 1)] by b3, XXREAL_3: 4;

      end;

      

       b5: for k be Nat holds P[k] from NAT_1:sch 2( b1, b2);

      

       c1: (( Partial_Sums s) . ( len f)) >= 0 by a7, SUPINF_2: 51;

      per cases ;

        suppose

         c2: (( Partial_Sums s) . ( len f)) = +infty ;

        then for k be Element of NAT holds ((( Partial_Sums s) ^\ ( len f)) . k) >= +infty by b5;

        then (( Partial_Sums s) ^\ ( len f)) is convergent_to_+infty by RINFSUP2: 32;

        then ( lim (( Partial_Sums s) ^\ ( len f))) = +infty by MESFUNC5:def 12;

        hence ( Sum s) = ( Sum f) by a6, c2, a9, MESFUNC9:def 3;

        hence ( SUM s) = ( Sum f) by a7, MEASURE8: 2;

      end;

        suppose (( Partial_Sums s) . ( len f)) <> +infty ;

        then (( Partial_Sums s) . ( len f)) in REAL by c1, XXREAL_0: 14;

        then

        reconsider r = (( Partial_Sums s) . ( len f)) as Real;

        for k be Nat holds ((( Partial_Sums s) ^\ ( len f)) . k) = r by b5;

        then ( lim ( Partial_Sums s)) = ( Sum f) by a6, a9, MESFUNC5: 52;

        hence ( Sum s) = ( Sum f) by MESFUNC9:def 3;

        hence ( SUM s) = ( Sum f) by a7, MEASURE8: 2;

      end;

    end;

    theorem :: MEASUR10:37

    

     Th38: 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 holds for F be disjoint_valued FinSequence of ( measurable_rectangles (S1,S2)) st ( Union F) in ( measurable_rectangles (S1,S2)) holds (( product-pre-Measure (M1,M2)) . ( Union F)) = ( Sum (( product-pre-Measure (M1,M2)) * F))

    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;

      set S = ( measurable_rectangles (S1,S2));

      set P = ( product-pre-Measure (M1,M2));

      let F be disjoint_valued FinSequence of S;

      assume

       A1: ( Union F) in S;

      defpred P[ object, object] means ($1 in ( dom F) implies $2 = (F . $1)) & ( not $1 in ( dom F) implies $2 = {} );

      

       A2: for n be Element of NAT holds ex y be Element of S st P[n, y]

      proof

        let n be Element of NAT ;

        per cases ;

          suppose

           A3: n in ( dom F);

          then (F . n) in ( rng F) by FUNCT_1: 3;

          hence ex y be Element of S st P[n, y] by A3;

        end;

          suppose

           A4: not n in ( dom F);

           {} in S by SETFAM_1:def 8;

          hence ex y be Element of S st P[n, y] by A4;

        end;

      end;

      consider G be Function of NAT , S such that

       A5: for n be Element of NAT holds P[n, (G . n)] from FUNCT_2:sch 3( A2);

      

       A6: for x be object st not x in ( dom F) holds (G . x) = {}

      proof

        let x be object;

        assume

         A7: not x in ( dom F);

        per cases ;

          suppose x in ( dom G);

          hence (G . x) = {} by A5, A7;

        end;

          suppose not x in ( dom G);

          hence (G . x) = {} by FUNCT_1:def 2;

        end;

      end;

      for x,y be object st x <> y holds (G . x) misses (G . y)

      proof

        let x,y be object;

        assume

         A7: x <> y;

        per cases ;

          suppose x in ( dom F) & y in ( dom F);

          then (G . x) = (F . x) & (G . y) = (F . y) by A5;

          hence (G . x) misses (G . y) by A7, PROB_2:def 2;

        end;

          suppose not x in ( dom F) or not y in ( dom F);

          then (G . x) = {} or (G . y) = {} by A6;

          hence (G . x) misses (G . y);

        end;

      end;

      then

      reconsider G as disjoint_valued Function of NAT , ( measurable_rectangles (S1,S2)) by PROB_2:def 2;

      now

        let y be object;

        assume

         B1: y in (( rng F) \/ { {} });

        per cases by B1, XBOOLE_0:def 3;

          suppose y in ( rng F);

          then

          consider x be object such that

           A8: x in ( dom F) & y = (F . x) by FUNCT_1:def 3;

          y = (G . x) by A8, A5;

          hence y in ( rng G) by A8, FUNCT_2: 4;

        end;

          suppose y in { {} };

          then

           B3: y = {} by TARSKI:def 1;

           not 0 in ( dom F) by FINSEQ_3: 24;

          then (G . 0 ) = {} by A5;

          hence y in ( rng G) by B3, FUNCT_2: 4;

        end;

      end;

      then

       A10: (( rng F) \/ { {} }) c= ( rng G);

      now

        let y be object;

        assume y in ( rng G);

        then

        consider x be Element of NAT such that

         A11: y = (G . x) by FUNCT_2: 113;

        per cases ;

          suppose

           A12: x in ( dom F);

          then y = (F . x) by A5, A11;

          then y in ( rng F) by A12, FUNCT_1: 3;

          hence y in (( rng F) \/ { {} }) by XBOOLE_0:def 3;

        end;

          suppose not x in ( dom F);

          then y = {} by A5, A11;

          then y in { {} } by TARSKI:def 1;

          hence y in (( rng F) \/ { {} }) by XBOOLE_0:def 3;

        end;

      end;

      then ( rng G) c= (( rng F) \/ { {} });

      then (( rng F) \/ { {} }) = ( rng G) by A10;

      then (( union ( rng F)) \/ ( union { {} })) = ( union ( rng G)) by ZFMISC_1: 78;

      then (( union ( rng F)) \/ {} ) = ( union ( rng G)) by ZFMISC_1: 25;

      then ( Union F) = ( union ( rng G)) by CARD_3:def 4;

      then ( Union F) = ( Union G) by CARD_3:def 4;

      then

       P2: (( product-pre-Measure (M1,M2)) . ( Union F)) = ( SUM (( product-pre-Measure (M1,M2)) * G)) by A1, Th35;

      

       P3: (( product-pre-Measure (M1,M2)) * F) is nonnegative FinSequence of ExtREAL by MEASURE9: 47;

      

       P4: for n be object st n in ( dom (( product-pre-Measure (M1,M2)) * F)) holds ((( product-pre-Measure (M1,M2)) * F) . n) = ((( product-pre-Measure (M1,M2)) * G) . n)

      proof

        let n be object;

        assume

         Q1: n in ( dom (( product-pre-Measure (M1,M2)) * F));

        

         Q5: ( dom G) = NAT by FUNCT_2:def 1;

        (F . n) = (G . n) by A5, Q1, FUNCT_1: 11;

        then ((( product-pre-Measure (M1,M2)) * F) . n) = (( product-pre-Measure (M1,M2)) . (G . n)) by Q1, FUNCT_1: 12;

        hence thesis by Q5, Q1, FUNCT_1: 13;

      end;

      for n be Element of NAT st not n in ( dom (( product-pre-Measure (M1,M2)) * F)) holds ((( product-pre-Measure (M1,M2)) * G) . n) = 0

      proof

        let n be Element of NAT ;

        assume

         L1: not n in ( dom (( product-pre-Measure (M1,M2)) * F));

        

         L2: ( dom ( product-pre-Measure (M1,M2))) = ( measurable_rectangles (S1,S2)) by FUNCT_2:def 1;

        n in NAT ;

        then

         L4: n in ( dom G) by FUNCT_2:def 1;

        now

          assume not (F . n) in ( dom ( product-pre-Measure (M1,M2)));

          then not (F . n) in ( rng F) by L2;

          hence not n in ( dom F) by FUNCT_1: 3;

        end;

        then (G . n) = {} by A5, L1, FUNCT_1: 11;

        then ((( product-pre-Measure (M1,M2)) * G) . n) = (( product-pre-Measure (M1,M2)) . {} ) by L4, FUNCT_1: 13;

        hence thesis by VALUED_0:def 19;

      end;

      hence thesis by P2, P3, P4, Th37;

    end;

    theorem :: MEASUR10:38

    

     Th39: 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 holds ( product-pre-Measure (M1,M2)) is pre-Measure of ( measurable_rectangles (S1,S2))

    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;

      set P = ( measurable_rectangles (S1,S2));

      set M = ( product-pre-Measure (M1,M2));

      

       A2: for F be disjoint_valued FinSequence of P st ( Union F) in P holds (M . ( Union F)) = ( Sum (M * F)) by Th38;

      for K be disjoint_valued Function of NAT , P st ( Union K) in P holds (M . ( Union K)) <= ( SUM (M * K)) by Th35;

      hence thesis by A2, MEASURE9:def 7;

    end;

    definition

      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;

      :: original: product-pre-Measure

      redefine

      func product-pre-Measure (M1,M2) -> pre-Measure of ( measurable_rectangles (S1,S2)) ;

      correctness by Th39;

    end