mesfunc4.miz



    begin

    theorem :: MESFUNC4:1

    

     Th1: for F,G,H be FinSequence of ExtREAL st F is nonnegative & G is nonnegative & ( dom F) = ( dom G) & H = (F + G) holds ( Sum H) = (( Sum F) + ( Sum G))

    proof

      let F,G,H be FinSequence of ExtREAL ;

      assume that

       A1: F is nonnegative and

       A2: G is nonnegative and

       A3: ( dom F) = ( dom G) and

       A4: H = (F + G);

      for y be object st y in ( rng F) holds not y in { -infty }

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A5: x in ( dom F) and

         A6: y = (F . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A5;

         0. <= (F . x) by A1, SUPINF_2: 39;

        hence thesis by A6, TARSKI:def 1;

      end;

      then ( rng F) misses { -infty } by XBOOLE_0: 3;

      then

       A7: (F " { -infty }) = {} by RELAT_1: 138;

      for y be object st y in ( rng G) holds not y in { -infty }

      proof

        let y be object;

        assume y in ( rng G);

        then

        consider x be object such that

         A8: x in ( dom G) and

         A9: y = (G . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A8;

         0. <= (G . x) by A2, SUPINF_2: 39;

        hence thesis by A9, TARSKI:def 1;

      end;

      then ( rng G) misses { -infty } by XBOOLE_0: 3;

      then

       A10: (G " { -infty }) = {} by RELAT_1: 138;

      

       A11: ( dom H) = ((( dom F) /\ ( dom G)) \ (((F " { -infty }) /\ (G " { +infty })) \/ ((F " { +infty }) /\ (G " { -infty })))) by A4, MESFUNC1:def 3

      .= ( dom F) by A3, A7, A10;

      then

       A12: ( len H) = ( len F) by FINSEQ_3: 29;

      consider h be sequence of ExtREAL such that

       A13: ( Sum H) = (h . ( len H)) and

       A14: (h . 0 ) = 0. and

       A15: for i be Nat st i < ( len H) holds (h . (i + 1)) = ((h . i) + (H . (i + 1))) by EXTREAL1:def 2;

      consider f be sequence of ExtREAL such that

       A16: ( Sum F) = (f . ( len F)) and

       A17: (f . 0 ) = 0. and

       A18: for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1))) by EXTREAL1:def 2;

      consider g be sequence of ExtREAL such that

       A19: ( Sum G) = (g . ( len G)) and

       A20: (g . 0 ) = 0. and

       A21: for i be Nat st i < ( len G) holds (g . (i + 1)) = ((g . i) + (G . (i + 1))) by EXTREAL1:def 2;

      defpred P[ Nat] means $1 <= ( len H) implies (h . $1) = ((f . $1) + (g . $1));

      

       A22: ( len H) = ( len G) by A3, A11, FINSEQ_3: 29;

      

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

      proof

        let k be Nat;

        assume

         A24: P[k];

        assume

         A25: (k + 1) <= ( len H);

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

        

         A26: k < ( len H) by A25, NAT_1: 13;

        then

         A27: (f . (k + 1)) = ((f . k) + (F . (k + 1))) & (g . (k + 1)) = ((g . k) + (G . (k + 1))) by A18, A21, A12, A22;

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

        then

         A28: (k + 1) in ( dom H) by A25, FINSEQ_3: 25;

        

         A29: (f . k) <> -infty & (g . k) <> -infty & (F . (k + 1)) <> -infty & (G . (k + 1)) <> -infty

        proof

          defpred Pg[ Nat] means $1 <= ( len H) implies (g . $1) <> -infty ;

          defpred Pf[ Nat] means $1 <= ( len H) implies (f . $1) <> -infty ;

          

           A30: for m be Nat st Pf[m] holds Pf[(m + 1)]

          proof

            let m be Nat;

            assume

             A31: Pf[m];

            assume

             A32: (m + 1) <= ( len H);

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

            

             A33: 0. <= (F . (m + 1)) by A1, SUPINF_2: 39;

            m < ( len H) by A32, NAT_1: 13;

            then (f . (m + 1)) = ((f . m) + (F . (m + 1))) by A18, A12;

            hence thesis by A31, A32, A33, NAT_1: 13, XXREAL_3: 17;

          end;

          

           A34: Pf[ 0 ] by A17;

          for i be Nat holds Pf[i] from NAT_1:sch 2( A34, A30);

          hence (f . k) <> -infty by A26;

          

           A35: for m be Nat st Pg[m] holds Pg[(m + 1)]

          proof

            let m be Nat;

            assume

             A36: Pg[m];

            assume

             A37: (m + 1) <= ( len H);

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

            

             A38: 0. <= (G . (m + 1)) by A2, SUPINF_2: 39;

            m < ( len H) by A37, NAT_1: 13;

            then (g . (m + 1)) = ((g . m) + (G . (m + 1))) by A21, A22;

            hence thesis by A36, A37, A38, NAT_1: 13, XXREAL_3: 17;

          end;

          

           A39: Pg[ 0 ] by A20;

          for i be Nat holds Pg[i] from NAT_1:sch 2( A39, A35);

          hence (g . k) <> -infty by A26;

          thus (F . (k + 1)) <> -infty by A1, SUPINF_2: 51;

          thus thesis by A2, SUPINF_2: 51;

        end;

        then

         A40: ((f . k) + (F . (k + 1))) <> -infty by XXREAL_3: 17;

        

         A41: (h . (k + 1)) = (((f . k) + (g . k)) + (H . (k + 1))) by A15, A24, A26

        .= (((f . k) + (g . k)) + ((F . (k + 1)) + (G . (k + 1)))) by A4, A28, MESFUNC1:def 3;

        ((f . k) + (g . k)) <> -infty by A29, XXREAL_3: 17;

        

        then (h . (k + 1)) = ((((f . k) + (g . k)) + (F . (k + 1))) + (G . (k + 1))) by A41, A29, XXREAL_3: 29

        .= ((((f . k) + (F . (k + 1))) + (g . k)) + (G . (k + 1))) by A29, XXREAL_3: 29

        .= ((f . (k + 1)) + (g . (k + 1))) by A27, A29, A40, XXREAL_3: 29;

        hence thesis;

      end;

      

       A42: P[ 0 ] by A17, A20, A14;

      for i be Nat holds P[i] from NAT_1:sch 2( A42, A23);

      hence thesis by A16, A19, A13, A12, A22;

    end;

    theorem :: MESFUNC4:2

    

     Th2: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S holds for n be Nat, f be PartFunc of X, ExtREAL , F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL st f is_simple_func_in S & ( dom f) <> {} & f is nonnegative & (F,a) are_Re-presentation_of f & ( dom x) = ( dom F) & (for i be Nat st i in ( dom x) holds (x . i) = ((a . i) * ((M * F) . i))) & ( len F) = n holds ( integral (M,f)) = ( Sum x)

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      defpred P[ Nat] means for f be PartFunc of X, ExtREAL , F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL st f is_simple_func_in S & ( dom f) <> {} & f is nonnegative & (F,a) are_Re-presentation_of f & ( dom x) = ( dom F) & (for i be Nat st i in ( dom x) holds (x . i) = ((a . i) * ((M * F) . i))) & ( len F) = $1 holds ( integral (M,f)) = ( Sum x);

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: P[n];

        let f be PartFunc of X, ExtREAL , F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL such that

         A3: f is_simple_func_in S and

         A4: ( dom f) <> {} and

         A5: f is nonnegative and

         A6: (F,a) are_Re-presentation_of f and

         A7: ( dom x) = ( dom F) and

         A8: for i be Nat st i in ( dom x) holds (x . i) = ((a . i) * ((M * F) . i)) and

         A9: ( len F) = (n + 1);

        

         A10: f is real-valued by A3, MESFUNC2:def 4;

        

         a5: for x be object st x in ( dom f) holds 0. <= (f . x) by A5, SUPINF_2: 51;

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

        set F1 = (F | ( Seg n));

        set f1 = (f | ( union ( rng F1)));

        reconsider F1 as Finite_Sep_Sequence of S by MESFUNC2: 33;

        

         A11: ( dom f1) = (( dom f) /\ ( union ( rng F1))) by RELAT_1: 61

        .= (( union ( rng F)) /\ ( union ( rng F1))) by A6, MESFUNC3:def 1;

        for x be object st x in ( dom f1) holds 0. <= (f1 . x)

        proof

          let x be object;

          assume x in ( dom f1);

          then

           X: ( dom f1) c= ( dom f) & (f1 . x) = (f . x) by FUNCT_1: 47, RELAT_1: 60;

           0. <= (f . x) by A5, SUPINF_2: 51;

          hence thesis by X;

        end;

        then

         a12: f1 is nonnegative by SUPINF_2: 52;

        set a1 = (a | ( Seg n));

        reconsider a1 as FinSequence of ExtREAL by FINSEQ_1: 18;

        set x1 = (x | ( Seg n));

        reconsider x1 as FinSequence of ExtREAL by FINSEQ_1: 18;

        

         A14: ( dom x1) = (( dom F) /\ ( Seg n)) by A7, RELAT_1: 61

        .= ( dom F1) by RELAT_1: 61;

        

         A15: ( union ( rng F1)) c= ( union ( rng F)) by RELAT_1: 70, ZFMISC_1: 77;

        then

         A16: ( dom f1) = ( union ( rng F1)) by A11, XBOOLE_1: 28;

        ex F19 be Finite_Sep_Sequence of S st (( dom f1) = ( union ( rng F19)) & for n be Nat, x,y be Element of X st n in ( dom F19) & x in (F19 . n) & y in (F19 . n) holds (f1 . x) = (f1 . y))

        proof

          take F1;

          for n be Nat, x,y be Element of X st n in ( dom F1) & x in (F1 . n) & y in (F1 . n) holds (f1 . x) = (f1 . y)

          proof

            let n be Nat;

            let x,y be Element of X;

            assume that

             A17: n in ( dom F1) and

             A18: x in (F1 . n) and

             A19: y in (F1 . n);

            (F1 . n) c= ( dom f1) by A16, A17, FUNCT_1: 3, ZFMISC_1: 74;

            then

             A20: (f1 . x) = (f . x) & (f1 . y) = (f . y) by A18, A19, FUNCT_1: 47;

            

             A21: ( dom F1) c= ( dom F) by RELAT_1: 60;

            

             A22: (F1 . n) = (F . n) by A17, FUNCT_1: 47;

            then (f . x) = (a . n) by A6, A17, A18, A21, MESFUNC3:def 1;

            hence thesis by A6, A17, A19, A20, A22, A21, MESFUNC3:def 1;

          end;

          hence thesis by A11, A15, XBOOLE_1: 28;

        end;

        then

         A23: f1 is_simple_func_in S by A10, MESFUNC2:def 4;

        

         A24: ( dom F1) = (( dom F) /\ ( Seg n)) by RELAT_1: 61

        .= (( dom a) /\ ( Seg n)) by A6, MESFUNC3:def 1

        .= ( dom a1) by RELAT_1: 61;

        for n be Nat st n in ( dom F1) holds for x be object st x in (F1 . n) holds (f1 . x) = (a1 . n)

        proof

          let n be Nat;

          assume

           A25: n in ( dom F1);

          then

           A26: (F1 . n) = (F . n) & (a1 . n) = (a . n) by A24, FUNCT_1: 47;

          let x be object;

          assume

           A27: x in (F1 . n);

          (F1 . n) c= ( dom f1) by A16, A25, FUNCT_1: 3, ZFMISC_1: 74;

          then ( dom F1) c= ( dom F) & (f1 . x) = (f . x) by A27, FUNCT_1: 47, RELAT_1: 60;

          hence thesis by A6, A25, A26, A27, MESFUNC3:def 1;

        end;

        then

         A28: (F1,a1) are_Re-presentation_of f1 by A16, A24, MESFUNC3:def 1;

        now

          per cases ;

            suppose

             A29: ( dom f1) = {} ;

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

            then

             A30: (n + 1) in ( dom F) by A9, FINSEQ_3: 25;

            

             A31: ( union ( rng F)) = (( union ( rng F1)) \/ (F . (n + 1)))

            proof

              thus ( union ( rng F)) c= (( union ( rng F1)) \/ (F . (n + 1)))

              proof

                let v be object;

                assume v in ( union ( rng F));

                then

                consider A be set such that

                 A32: v in A and

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

                consider i be object such that

                 A34: i in ( dom F) and

                 A35: A = (F . i) by A33, FUNCT_1:def 3;

                reconsider i as Element of NAT by A34;

                

                 A36: i in ( Seg ( len F)) by A34, FINSEQ_1:def 3;

                then

                 A37: 1 <= i by FINSEQ_1: 1;

                

                 A38: i <= (n + 1) by A9, A36, FINSEQ_1: 1;

                per cases ;

                  suppose i = (n + 1);

                  hence thesis by A32, A35, XBOOLE_0:def 3;

                end;

                  suppose i <> (n + 1);

                  then i < (n + 1) by A38, XXREAL_0: 1;

                  then i <= n by NAT_1: 13;

                  then i in ( Seg n) by A37, FINSEQ_1: 1;

                  then i in (( dom F) /\ ( Seg n)) by A34, XBOOLE_0:def 4;

                  then i in ( dom F1) by RELAT_1: 61;

                  then (F1 . i) = A & (F1 . i) in ( rng F1) by A35, FUNCT_1: 3, FUNCT_1: 47;

                  then v in ( union ( rng F1)) by A32, TARSKI:def 4;

                  hence thesis by XBOOLE_0:def 3;

                end;

              end;

              let v be object;

              assume

               A39: v in (( union ( rng F1)) \/ (F . (n + 1)));

              per cases by A39, XBOOLE_0:def 3;

                suppose v in ( union ( rng F1));

                then

                consider A be set such that

                 A40: v in A and

                 A41: A in ( rng F1) by TARSKI:def 4;

                consider i be object such that

                 A42: i in ( dom F1) and

                 A43: A = (F1 . i) by A41, FUNCT_1:def 3;

                i in (( dom F) /\ ( Seg n)) by A42, RELAT_1: 61;

                then

                 A44: i in ( dom F) by XBOOLE_0:def 4;

                (F . i) = A by A42, A43, FUNCT_1: 47;

                then A in ( rng F) by A44, FUNCT_1: 3;

                hence thesis by A40, TARSKI:def 4;

              end;

                suppose

                 A45: v in (F . (n + 1));

                (F . (n + 1)) in ( rng F) by A30, FUNCT_1: 3;

                hence thesis by A45, TARSKI:def 4;

              end;

            end;

            

             A46: ( Seg ( len x)) = ( dom F) by A7, FINSEQ_1:def 3

            .= ( Seg (n + 1)) by A9, FINSEQ_1:def 3;

            then

             A47: ( len x) = (n + 1) by FINSEQ_1: 6;

            then

             A48: n < ( len x) by NAT_1: 13;

            consider sumx be sequence of ExtREAL such that

             A49: ( Sum x) = (sumx . ( len x)) and

             A50: (sumx . 0 ) = 0. and

             A51: for m be Nat st m < ( len x) holds (sumx . (m + 1)) = ((sumx . m) + (x . (m + 1))) by EXTREAL1:def 2;

            defpred PSumx[ Nat] means $1 < ( len x) implies (sumx . $1) = 0. ;

            

             A52: for m be Nat st m in ( dom F1) holds (F1 . m) = {}

            proof

              let m be Nat;

              assume m in ( dom F1);

              then (F1 . m) in ( rng F1) by FUNCT_1: 3;

              hence thesis by A16, A29, XBOOLE_1: 3, ZFMISC_1: 74;

            end;

            

             A53: for m be Nat st m in ( dom F1) holds (x . m) = 0.

            proof

              reconsider EMPTY = {} as Element of S by PROB_1: 4;

              let m be Nat;

              assume

               A54: m in ( dom F1);

              then (F1 . m) = {} by A52;

              then

               A55: (F . m) = {} by A54, FUNCT_1: 47;

              m in (( dom F) /\ ( Seg n)) by A54, RELAT_1: 61;

              then

               A56: m in ( dom x) by A7, XBOOLE_0:def 4;

              then

               A57: (x . m) = ((a . m) * ((M * F) . m)) by A8;

              (M . EMPTY) = 0. by VALUED_0:def 19;

              then ((M * F) . m) = 0. by A7, A56, A55, FUNCT_1: 13;

              hence thesis by A57;

            end;

            

             A58: for m be Nat st PSumx[m] holds PSumx[(m + 1)]

            proof

              let m be Nat;

              assume

               A59: PSumx[m];

              

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

              assume

               A61: (m + 1) < ( len x);

              then (m + 1) <= n by A47, NAT_1: 13;

              then

               A62: (m + 1) in ( Seg n) by A60, FINSEQ_1: 1;

              (m + 1) in ( Seg ( len x)) by A61, A60, FINSEQ_1: 1;

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

              then (m + 1) in (( dom F) /\ ( Seg n)) by A62, XBOOLE_0:def 4;

              then

               A63: (m + 1) in ( dom F1) by RELAT_1: 61;

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

              then m < ( len x) by A61, XXREAL_0: 2;

              

              then (sumx . (m + 1)) = ( 0. + (x . (m + 1))) by A51, A59

              .= (x . (m + 1)) by XXREAL_3: 4;

              hence thesis by A53, A63;

            end;

            

             A64: PSumx[ 0 ] by A50;

            

             A65: for m be Nat holds PSumx[m] from NAT_1:sch 2( A64, A58);

            

             A66: ( Sum x) = (sumx . (n + 1)) by A49, A46, FINSEQ_1: 6

            .= ((sumx . n) + (x . (n + 1))) by A51, A48

            .= ( 0. + (x . (n + 1))) by A65, A48

            .= (x . (n + 1)) by XXREAL_3: 4;

            now

              per cases ;

                case

                 A67: (a . (n + 1)) <> 0. ;

                defpred Pb[ Nat, set] means ($1 = 1 implies $2 = 0. ) & ($1 = 2 implies $2 = (a . (n + 1)));

                defpred PG[ Nat, set] means ($1 = 1 implies $2 = ( union ( rng F1))) & ($1 = 2 implies $2 = (F . (n + 1)));

                

                 A68: for k be Nat st k in ( Seg 2) holds ex x be Element of ExtREAL st Pb[k, x]

                proof

                  let k be Nat;

                  assume

                   A69: k in ( Seg 2);

                  per cases by A69, FINSEQ_1: 2, TARSKI:def 2;

                    suppose

                     A70: k = 1;

                    set x = 0. ;

                    reconsider x as Element of ExtREAL ;

                    take x;

                    thus thesis by A70;

                  end;

                    suppose

                     A71: k = 2;

                    set x = (a . (n + 1));

                    reconsider x as Element of ExtREAL ;

                    take x;

                    thus thesis by A71;

                  end;

                end;

                consider b be FinSequence of ExtREAL such that

                 A72: ( dom b) = ( Seg 2) & for k be Nat st k in ( Seg 2) holds Pb[k, (b . k)] from FINSEQ_1:sch 5( A68);

                

                 A73: for k be Nat st k in ( Seg 2) holds ex x be Element of S st PG[k, x]

                proof

                  let k be Nat;

                  assume

                   A74: k in ( Seg 2);

                  per cases by A74, FINSEQ_1: 2, TARSKI:def 2;

                    suppose

                     A75: k = 1;

                    set x = ( union ( rng F1));

                    reconsider x as Element of S by MESFUNC2: 31;

                    take x;

                    thus thesis by A75;

                  end;

                    suppose

                     A76: k = 2;

                    set x = (F . (n + 1));

                    (F . (n + 1)) in ( rng F) & ( rng F) c= S by A30, FINSEQ_1:def 4, FUNCT_1: 3;

                    then

                    reconsider x as Element of S;

                    take x;

                    thus thesis by A76;

                  end;

                end;

                consider G be FinSequence of S such that

                 A77: ( dom G) = ( Seg 2) & for k be Nat st k in ( Seg 2) holds PG[k, (G . k)] from FINSEQ_1:sch 5( A73);

                

                 A78: 1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A79: (b . 1) = 0. by A72;

                

                 A80: (b . 1) = 0. by A72, A78;

                2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A81: (b . 2) = (a . (n + 1)) by A72;

                

                 A82: 2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A83: (G . 2) = (F . (n + 1)) by A77;

                

                 A84: 1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A85: (G . 1) = ( union ( rng F1)) by A77;

                

                 A86: for u,v be object st u <> v holds (G . u) misses (G . v)

                proof

                  let u,v be object;

                  assume

                   A87: u <> v;

                  per cases ;

                    suppose

                     A88: u in ( dom G) & v in ( dom G);

                    then

                     A89: u = 1 or u = 2 by A77, FINSEQ_1: 2, TARSKI:def 2;

                    per cases by A77, A87, A88, A89, FINSEQ_1: 2, TARSKI:def 2;

                      suppose

                       A90: u = 1 & v = 2;

                      assume (G . u) meets (G . v);

                      then

                      consider z be object such that

                       A91: z in (G . u) and

                       A92: z in (G . v) by XBOOLE_0: 3;

                      consider A be set such that

                       A93: z in A and

                       A94: A in ( rng F1) by A85, A90, A91, TARSKI:def 4;

                      consider k9 be object such that

                       A95: k9 in ( dom F1) and

                       A96: A = (F1 . k9) by A94, FUNCT_1:def 3;

                      reconsider k9 as Element of NAT by A95;

                      

                       A97: z in (F . k9) by A93, A95, A96, FUNCT_1: 47;

                      k9 in (( dom F) /\ ( Seg n)) by A95, RELAT_1: 61;

                      then k9 in ( Seg n) by XBOOLE_0:def 4;

                      then k9 <= n by FINSEQ_1: 1;

                      then k9 < (n + 1) by NAT_1: 13;

                      then

                       A98: (F . k9) misses (F . (n + 1)) by PROB_2:def 2;

                      z in (F . (n + 1)) by A77, A82, A90, A92;

                      hence contradiction by A98, A97, XBOOLE_0: 3;

                    end;

                      suppose

                       A99: u = 2 & v = 1;

                      assume (G . u) meets (G . v);

                      then

                      consider z be object such that

                       A100: z in (G . u) and

                       A101: z in (G . v) by XBOOLE_0: 3;

                      consider A be set such that

                       A102: z in A and

                       A103: A in ( rng F1) by A85, A99, A101, TARSKI:def 4;

                      consider k9 be object such that

                       A104: k9 in ( dom F1) and

                       A105: A = (F1 . k9) by A103, FUNCT_1:def 3;

                      reconsider k9 as Element of NAT by A104;

                      

                       A106: z in (F . k9) by A102, A104, A105, FUNCT_1: 47;

                      k9 in (( dom F) /\ ( Seg n)) by A104, RELAT_1: 61;

                      then k9 in ( Seg n) by XBOOLE_0:def 4;

                      then k9 <= n by FINSEQ_1: 1;

                      then k9 < (n + 1) by NAT_1: 13;

                      then

                       A107: (F . k9) misses (F . (n + 1)) by PROB_2:def 2;

                      z in (F . (n + 1)) by A77, A82, A99, A100;

                      hence contradiction by A107, A106, XBOOLE_0: 3;

                    end;

                  end;

                    suppose not u in ( dom G) or not v in ( dom G);

                    then (G . u) = {} or (G . v) = {} by FUNCT_1:def 2;

                    hence thesis;

                  end;

                end;

                ( len G) = 2 by A77, FINSEQ_1:def 3;

                then

                 A108: G = <*( union ( rng F1)), (F . (n + 1))*> by A85, A83, FINSEQ_1: 44;

                deffunc Fy( Nat) = ((b . $1) * ((M * G) . $1));

                consider y be FinSequence of ExtREAL such that

                 A109: ( len y) = 2 & for m be Nat st m in ( dom y) holds (y . m) = Fy(m) from FINSEQ_2:sch 1;

                

                 A110: ( dom y) = ( Seg 2) by A109, FINSEQ_1:def 3;

                1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A111: (y . 1) = ((b . 1) * ((M * G) . 1)) by A109, A110;

                consider sumy be sequence of ExtREAL such that

                 A112: ( Sum y) = (sumy . ( len y)) and

                 A113: (sumy . 0 ) = 0. and

                 A114: for k be Nat st k < ( len y) holds (sumy . (k + 1)) = ((sumy . k) + (y . (k + 1))) by EXTREAL1:def 2;

                

                 A115: (sumy . 1) = ((sumy . 0 ) + (y . ( 0 + 1))) by A109, A114

                .= 0. by A79, A111, A113;

                

                 A116: 2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                

                then ((M * G) . 2) = (M . (F . (n + 1))) by A77, A83, FUNCT_1: 13

                .= ((M * F) . (n + 1)) by A30, FUNCT_1: 13;

                then (y . 2) = ((a . (n + 1)) * ((M * F) . (n + 1))) by A81, A109, A110, A116;

                then

                 A117: (y . 2) = (x . (n + 1)) by A7, A8, A30;

                reconsider G as Finite_Sep_Sequence of S by A86, PROB_2:def 2;

                

                 A118: ( dom y) = ( dom G) by A77, A109, FINSEQ_1:def 3;

                

                 A119: for k be Nat st k in ( dom G) holds for v be object st v in (G . k) holds (f . v) = (b . k)

                proof

                  let k be Nat;

                  assume

                   A120: k in ( dom G);

                  let v be object;

                  assume

                   A121: v in (G . k);

                  per cases by A77, A120, FINSEQ_1: 2, TARSKI:def 2;

                    suppose k = 1;

                    hence thesis by A16, A29, A77, A84, A121;

                  end;

                    suppose k = 2;

                    hence thesis by A6, A30, A83, A81, A121, MESFUNC3:def 1;

                  end;

                end;

                

                 A122: for k be Nat st 2 <= k & k in ( dom b) holds 0. < (b . k) & (b . k) < +infty

                proof

                  let k be Nat;

                  assume that

                   A123: 2 <= k and

                   A124: k in ( dom b);

                  

                   A125: k = 1 or k = 2 by A72, A124, FINSEQ_1: 2, TARSKI:def 2;

                  then (G . k) <> {} by A4, A6, A11, A29, A31, A83, A123, MESFUNC3:def 1;

                  then

                  consider v be object such that

                   A126: v in (G . k) by XBOOLE_0:def 1;

                  

                   A127: v in ( dom f) by A6, A16, A29, A31, A83, A123, A125, A126, MESFUNC3:def 1;

                  

                   A128: (f . v) = (b . k) by A77, A72, A119, A124, A126;

                  hence 0. < (b . k) by A67, A81, A123, A125, A127, a5;

                  ( dom f) c= X by RELAT_1:def 18;

                  then

                  reconsider v as Element of X by A127;

                   |.(f . v).| < +infty by A10, A127, MESFUNC2:def 1;

                  hence thesis by A128, EXTREAL1: 21;

                end;

                ( dom f) = (( union ( rng F1)) \/ (F . (n + 1))) by A6, A31, MESFUNC3:def 1

                .= ( union {( union ( rng F1)), (F . (n + 1))}) by ZFMISC_1: 75

                .= ( union ( rng G)) by A108, FINSEQ_2: 127;

                then

                 A129: (G,b) are_Re-presentation_of f by A77, A72, A119, MESFUNC3:def 1;

                ( Sum y) = (sumy . (1 + 1)) by A109, A112

                .= ( 0. + (x . (n + 1))) by A109, A117, A114, A115

                .= (x . (n + 1)) by XXREAL_3: 4;

                hence thesis by A3, A5, A66, A109, A122, A129, A80, A118, MESFUNC3:def 2;

              end;

                case

                 A130: (a . (n + 1)) = 0. ;

                defpred Pb[ Nat, set] means ($1 = 1 implies $2 = 0. ) & ($1 = 2 implies $2 = 1. );

                defpred PG[ Nat, set] means ($1 = 1 implies $2 = ( union ( rng F))) & ($1 = 2 implies $2 = {} );

                

                 A131: for k be Nat st k in ( Seg 2) holds ex v be Element of S st PG[k, v]

                proof

                  let k be Nat;

                  assume

                   A132: k in ( Seg 2);

                  per cases by A132, FINSEQ_1: 2, TARSKI:def 2;

                    suppose

                     A133: k = 1;

                    set v = ( union ( rng F));

                    reconsider v as Element of S by MESFUNC2: 31;

                    take v;

                    thus thesis by A133;

                  end;

                    suppose

                     A134: k = 2;

                    reconsider v = {} as Element of S by PROB_1: 4;

                    take v;

                    thus thesis by A134;

                  end;

                end;

                consider G be FinSequence of S such that

                 A135: ( dom G) = ( Seg 2) & for k be Nat st k in ( Seg 2) holds PG[k, (G . k)] from FINSEQ_1:sch 5( A131);

                

                 A136: for u,v be object st u <> v holds (G . u) misses (G . v)

                proof

                  let u,v be object;

                  assume

                   A137: u <> v;

                  per cases ;

                    suppose

                     A138: u in ( dom G) & v in ( dom G);

                    then

                     A139: u = 1 or u = 2 by A135, FINSEQ_1: 2, TARSKI:def 2;

                    per cases by A135, A137, A138, A139, FINSEQ_1: 2, TARSKI:def 2;

                      suppose u = 1 & v = 2;

                      then (G . v) = {} by A135, A138;

                      hence thesis;

                    end;

                      suppose u = 2 & v = 1;

                      then (G . u) = {} by A135, A138;

                      hence thesis;

                    end;

                  end;

                    suppose not u in ( dom G) or not v in ( dom G);

                    then (G . u) = {} or (G . v) = {} by FUNCT_1:def 2;

                    hence thesis;

                  end;

                end;

                

                 A140: for k be Nat st k in ( Seg 2) holds ex v be Element of ExtREAL st Pb[k, v]

                proof

                  let k be Nat;

                  assume

                   A141: k in ( Seg 2);

                  per cases by A141, FINSEQ_1: 2, TARSKI:def 2;

                    suppose

                     A142: k = 1;

                    set v = 0. ;

                    reconsider v as Element of ExtREAL ;

                    take v;

                    thus thesis by A142;

                  end;

                    suppose

                     A143: k = 2;

                    set v = 1. ;

                    reconsider v as Element of ExtREAL ;

                    take v;

                    thus thesis by A143;

                  end;

                end;

                consider b be FinSequence of ExtREAL such that

                 A144: ( dom b) = ( Seg 2) & for k be Nat st k in ( Seg 2) holds Pb[k, (b . k)] from FINSEQ_1:sch 5( A140);

                

                 A145: 2 in ( dom G) by A135, FINSEQ_1: 2, TARSKI:def 2;

                then

                 A146: (G . 2) = {} by A135;

                (M . (G . 2)) = ((M * G) . 2) by A145, FUNCT_1: 13;

                then

                 A147: ((M * G) . 2) = 0. by A146, VALUED_0:def 19;

                1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A148: (G . 1) = ( union ( rng F)) by A135;

                

                 A149: 1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A150: (b . 1) = 0. by A144;

                deffunc Fy( Nat) = ((b . $1) * ((M * G) . $1));

                consider y be FinSequence of ExtREAL such that

                 A151: ( len y) = 2 & for k be Nat st k in ( dom y) holds (y . k) = Fy(k) from FINSEQ_2:sch 1;

                

                 A152: ( dom y) = ( Seg 2) by A151, FINSEQ_1:def 3;

                2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A153: (y . 2) = ((b . 2) * ((M * G) . 2)) by A151, A152;

                1 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                then

                 A154: (y . 1) = ((b . 1) * ((M * G) . 1)) by A151, A152;

                reconsider G as Finite_Sep_Sequence of S by A136, PROB_2:def 2;

                

                 A155: ( dom y) = ( dom G) by A135, A151, FINSEQ_1:def 3;

                

                 A156: for k be Nat st k in ( dom G) holds for v be object st v in (G . k) holds (f . v) = (b . k)

                proof

                  let k be Nat;

                  assume

                   A157: k in ( dom G);

                  let v be object;

                  assume

                   A158: v in (G . k);

                  per cases by A135, A157, FINSEQ_1: 2, TARSKI:def 2;

                    suppose

                     A159: k = 1;

                    then (f . v) = 0. by A6, A16, A29, A30, A31, A130, A148, A158, MESFUNC3:def 1;

                    hence thesis by A144, A149, A159;

                  end;

                    suppose k = 2;

                    hence thesis by A135, A145, A158;

                  end;

                end;

                ( len G) = 2 by A135, FINSEQ_1:def 3;

                then G = <*( union ( rng F)), {} *> by A148, A146, FINSEQ_1: 44;

                then ( rng G) = {( union ( rng F)), {} } by FINSEQ_2: 127;

                

                then ( union ( rng G)) = (( union ( rng F)) \/ {} ) by ZFMISC_1: 75

                .= ( dom f) by A6, MESFUNC3:def 1;

                then

                 A160: (G,b) are_Re-presentation_of f by A135, A144, A156, MESFUNC3:def 1;

                consider sumy be sequence of ExtREAL such that

                 A161: ( Sum y) = (sumy . ( len y)) and

                 A162: (sumy . 0 ) = 0. and

                 A163: for k be Nat st k < ( len y) holds (sumy . (k + 1)) = ((sumy . k) + (y . (k + 1))) by EXTREAL1:def 2;

                

                 A164: (sumy . 1) = ((sumy . 0 ) + (y . ( 0 + 1))) by A151, A163

                .= 0. by A150, A154, A162;

                

                 A165: 2 in ( Seg 2) by FINSEQ_1: 2, TARSKI:def 2;

                

                 A166: for k be Nat st 2 <= k & k in ( dom b) holds 0. < (b . k) & (b . k) < +infty

                proof

                  let k be Nat;

                  assume that

                   A167: 2 <= k and

                   A168: k in ( dom b);

                  k = 1 or k = 2 by A144, A168, FINSEQ_1: 2, TARSKI:def 2;

                  hence 0. < (b . k) by A144, A165, A167;

                  

                   A169: 1 in REAL by NUMBERS: 19;

                   Pb[k, (b . k)] by A144, A149, A165;

                  then (b . k) = 1 or (b . k) = 0. by A144, A168, FINSEQ_1: 2, TARSKI:def 2;

                  hence thesis by XXREAL_0: 9, A169;

                end;

                

                 A170: (b . 1) = 0. by A144, A149;

                1 <= (n + 1) & (n + 1) <= ( len x) by A46, FINSEQ_1: 6, NAT_1: 11;

                then (n + 1) in ( dom x) by FINSEQ_3: 25;

                

                then

                 A171: (x . (n + 1)) = ((a . (n + 1)) * ((M * F) . (n + 1))) by A8

                .= 0. by A130;

                ( Sum y) = ((sumy . 1) + (y . (1 + 1))) by A151, A161, A163

                .= 0. by A147, A153, A164;

                hence thesis by A3, A5, A66, A171, A151, A166, A160, A170, A155, MESFUNC3:def 2;

              end;

            end;

            hence thesis;

          end;

            suppose

             A172: ( dom f1) <> {} ;

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

            then

             A173: ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

            

             A174: ( dom F) = ( Seg (n + 1)) by A9, FINSEQ_1:def 3;

            then ( dom F1) = (( Seg (n + 1)) /\ ( Seg n)) by RELAT_1: 61;

            then

             A175: ( dom F1) = ( Seg n) by A173, XBOOLE_1: 28;

            then

             A176: ( len F1) = n by FINSEQ_1:def 3;

            consider G be Finite_Sep_Sequence of S, b,y be FinSequence of ExtREAL such that

             A177: (G,b) are_Re-presentation_of f1 and

             A178: (b . 1) = 0. and

             A179: for n be Nat st 2 <= n & n in ( dom b) holds 0. < (b . n) & (b . n) < +infty and

             A180: ( dom y) = ( dom G) and

             A181: for n be Nat st n in ( dom y) holds (y . n) = ((b . n) * ((M * G) . n)) and

             A182: ( integral (M,f1)) = ( Sum y) by A23, MESFUNC3:def 2, a12;

            

             A183: for i be Nat st i in ( dom x1) holds (x1 . i) = ((a1 . i) * ((M * F1) . i))

            proof

              let i be Nat;

              assume

               A184: i in ( dom x1);

              

               A185: ( dom x1) c= ( dom x) by RELAT_1: 60;

              then (x . i) = ((a . i) * ((M * F) . i)) by A8, A184;

              

              then

               A186: (x1 . i) = ((a . i) * ((M * F) . i)) by A184, FUNCT_1: 47

              .= ((a1 . i) * ((M * F) . i)) by A24, A14, A184, FUNCT_1: 47;

              ((M * F) . i) = (M . (F . i)) by A7, A184, A185, FUNCT_1: 13

              .= (M . (F1 . i)) by A14, A184, FUNCT_1: 47

              .= ((M * F1) . i) by A14, A184, FUNCT_1: 13;

              hence thesis by A186;

            end;

            now

              per cases ;

                case

                 A187: (F . (n + 1)) = {} or (a . (n + 1)) = 0. ;

                defpred PH[ Nat, set] means ($1 = 1 implies $2 = ((G . 1) \/ (F . (n + 1)))) & (2 <= $1 implies $2 = (G . $1));

                

                 A188: for k be Nat st k in ( Seg ( len G)) holds ex x be Element of S st PH[k, x]

                proof

                  let k be Nat;

                  

                   A189: ( rng G) c= S by FINSEQ_1:def 4;

                  assume k in ( Seg ( len G));

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

                  then

                   A190: (G . k) in ( rng G) by FUNCT_1: 3;

                  per cases ;

                    suppose

                     A191: k = 1;

                    set x = ((G . 1) \/ (F . (n + 1)));

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

                    then (n + 1) in ( dom F) by A9, FINSEQ_3: 25;

                    then

                     A192: (F . (n + 1)) in ( rng F) by FUNCT_1: 3;

                    ( rng F) c= S by FINSEQ_1:def 4;

                    then

                    reconsider x as Element of S by A190, A189, A191, A192, FINSUB_1:def 1;

                     PH[k, x] by A191;

                    hence thesis;

                  end;

                    suppose

                     A193: k <> 1;

                    set x = (G . k);

                    reconsider x as Element of S by A190, A189;

                     PH[k, x] by A193;

                    hence thesis;

                  end;

                end;

                consider H be FinSequence of S such that

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

                

                 A195: for u,v be object st u <> v holds (H . u) misses (H . v)

                proof

                  let u,v be object;

                  assume

                   A196: u <> v;

                  per cases ;

                    suppose

                     A197: u in ( dom H) & v in ( dom H);

                    then

                    reconsider u1 = u, v1 = v as Element of NAT ;

                    per cases ;

                      suppose

                       A198: u = 1;

                      1 <= v1 by A194, A197, FINSEQ_1: 1;

                      then 1 < v1 by A196, A198, XXREAL_0: 1;

                      then

                       A199: (1 + 1) <= v1 by NAT_1: 13;

                      then

                       A200: (H . v) = (G . v) by A194, A197;

                      

                       A201: (F . (n + 1)) misses (G . v)

                      proof

                        per cases by A187;

                          suppose (F . (n + 1)) = {} ;

                          hence thesis;

                        end;

                          suppose

                           A202: (a . (n + 1)) = 0. ;

                          assume (F . (n + 1)) meets (G . v);

                          then

                          consider w be object such that

                           A203: w in (F . (n + 1)) and

                           A204: w in (G . v) by XBOOLE_0: 3;

                          

                           A205: v1 in ( dom G) by A194, A197, FINSEQ_1:def 3;

                          then

                           A206: v1 in ( dom b) by A177, MESFUNC3:def 1;

                          (G . v1) in ( rng G) by A205, FUNCT_1: 3;

                          then w in ( union ( rng G)) by A204, TARSKI:def 4;

                          then w in ( dom f1) by A177, MESFUNC3:def 1;

                          

                          then

                           A207: (f . w) = (f1 . w) by FUNCT_1: 47

                          .= (b . v1) by A177, A204, A205, MESFUNC3:def 1;

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

                          then (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 1;

                          then (n + 1) in ( dom F) by A9, FINSEQ_1:def 3;

                          then (f . w) = 0. by A6, A202, A203, MESFUNC3:def 1;

                          hence contradiction by A179, A199, A207, A206;

                        end;

                      end;

                      (H . u) = ((G . 1) \/ (F . (n + 1))) & (G . 1) misses (G . v) by A194, A196, A197, A198, PROB_2:def 2;

                      hence thesis by A200, A201, XBOOLE_1: 70;

                    end;

                      suppose

                       A208: u <> 1;

                      1 <= u1 by A194, A197, FINSEQ_1: 1;

                      then 1 < u1 by A208, XXREAL_0: 1;

                      then

                       A209: (1 + 1) <= u1 by NAT_1: 13;

                      then

                       A210: (H . u) = (G . u) by A194, A197;

                      per cases ;

                        suppose

                         A211: v = 1;

                        

                         A212: (F . (n + 1)) misses (G . u)

                        proof

                          per cases by A187;

                            suppose (F . (n + 1)) = {} ;

                            hence thesis;

                          end;

                            suppose

                             A213: (a . (n + 1)) = 0. ;

                            assume (F . (n + 1)) meets (G . u);

                            then

                            consider w be object such that

                             A214: w in (F . (n + 1)) and

                             A215: w in (G . u) by XBOOLE_0: 3;

                            

                             A216: u1 in ( dom G) by A194, A197, FINSEQ_1:def 3;

                            then

                             A217: u1 in ( dom b) by A177, MESFUNC3:def 1;

                            (G . u1) in ( rng G) by A216, FUNCT_1: 3;

                            then w in ( union ( rng G)) by A215, TARSKI:def 4;

                            then w in ( dom f1) by A177, MESFUNC3:def 1;

                            

                            then

                             A218: (f . w) = (f1 . w) by FUNCT_1: 47

                            .= (b . u1) by A177, A215, A216, MESFUNC3:def 1;

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

                            then (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 1;

                            then (n + 1) in ( dom F) by A9, FINSEQ_1:def 3;

                            then (f . w) = 0. by A6, A213, A214, MESFUNC3:def 1;

                            hence contradiction by A179, A209, A218, A217;

                          end;

                        end;

                        (H . v) = ((G . 1) \/ (F . (n + 1))) & (G . 1) misses (G . u) by A194, A196, A197, A211, PROB_2:def 2;

                        hence thesis by A210, A212, XBOOLE_1: 70;

                      end;

                        suppose

                         A219: v <> 1;

                        1 <= v1 by A194, A197, FINSEQ_1: 1;

                        then 1 < v1 by A219, XXREAL_0: 1;

                        then (1 + 1) <= v1 by NAT_1: 13;

                        then (H . v) = (G . v) by A194, A197;

                        hence thesis by A196, A210, PROB_2:def 2;

                      end;

                    end;

                  end;

                    suppose not u in ( dom H) or not v in ( dom H);

                    then (H . u) = {} or (H . v) = {} by FUNCT_1:def 2;

                    hence thesis;

                  end;

                end;

                deffunc Z( Nat) = ((b . $1) * ((M * H) . $1));

                reconsider H as Finite_Sep_Sequence of S by A195, PROB_2:def 2;

                consider z be FinSequence of ExtREAL such that

                 A220: ( len z) = ( len y) & for n be Nat st n in ( dom z) holds (z . n) = Z(n) from FINSEQ_2:sch 1;

                G <> {} by A172, A177, MESFUNC3:def 1, RELAT_1: 38, ZFMISC_1: 2;

                then ( 0 + 1) <= ( len G) by NAT_1: 13;

                then

                 A221: 1 in ( Seg ( len G)) by FINSEQ_1: 1;

                

                 A222: ( dom f) = ( union ( rng H))

                proof

                  thus ( dom f) c= ( union ( rng H))

                  proof

                    let v be object;

                    assume v in ( dom f);

                    then v in ( union ( rng F)) by A6, MESFUNC3:def 1;

                    then

                    consider A be set such that

                     A223: v in A and

                     A224: A in ( rng F) by TARSKI:def 4;

                    consider u be object such that

                     A225: u in ( dom F) and

                     A226: A = (F . u) by A224, FUNCT_1:def 3;

                    reconsider u as Element of NAT by A225;

                    

                     A227: u in ( Seg ( len F)) by A225, FINSEQ_1:def 3;

                    then

                     A228: 1 <= u by FINSEQ_1: 1;

                    

                     A229: u <= (n + 1) by A9, A227, FINSEQ_1: 1;

                    per cases ;

                      suppose u = (n + 1);

                      then (H . 1) = ((G . 1) \/ A) by A194, A221, A226;

                      then

                       A230: v in (H . 1) by A223, XBOOLE_0:def 3;

                      (H . 1) in ( rng H) by A194, A221, FUNCT_1: 3;

                      hence thesis by A230, TARSKI:def 4;

                    end;

                      suppose u <> (n + 1);

                      then u < (n + 1) by A229, XXREAL_0: 1;

                      then u <= n by NAT_1: 13;

                      then u in ( Seg n) by A228, FINSEQ_1: 1;

                      then (F1 . u) in ( rng F1) & A = (F1 . u) by A175, A226, FUNCT_1: 3, FUNCT_1: 47;

                      then v in ( union ( rng F1)) by A223, TARSKI:def 4;

                      then v in ( union ( rng G)) by A16, A177, MESFUNC3:def 1;

                      then

                      consider B be set such that

                       A231: v in B and

                       A232: B in ( rng G) by TARSKI:def 4;

                      consider w be object such that

                       A233: w in ( dom G) and

                       A234: B = (G . w) by A232, FUNCT_1:def 3;

                      reconsider w as Element of NAT by A233;

                      

                       A235: w in ( Seg ( len G)) by A233, FINSEQ_1:def 3;

                      per cases ;

                        suppose

                         A236: w = 1;

                        (H . 1) = ((G . 1) \/ (F . (n + 1))) by A194, A221;

                        then

                         A237: v in (H . 1) by A231, A234, A236, XBOOLE_0:def 3;

                        (H . 1) in ( rng H) by A194, A221, FUNCT_1: 3;

                        hence thesis by A237, TARSKI:def 4;

                      end;

                        suppose

                         A238: w <> 1;

                        1 <= w by A233, FINSEQ_3: 25;

                        then 1 < w by A238, XXREAL_0: 1;

                        then (1 + 1) <= w by NAT_1: 13;

                        then

                         A239: v in (H . w) by A194, A231, A234, A235;

                        (H . w) in ( rng H) by A194, A235, FUNCT_1: 3;

                        hence thesis by A239, TARSKI:def 4;

                      end;

                    end;

                  end;

                  let v be object;

                  assume v in ( union ( rng H));

                  then

                  consider A be set such that

                   A240: v in A and

                   A241: A in ( rng H) by TARSKI:def 4;

                  consider k be object such that

                   A242: k in ( dom H) and

                   A243: A = (H . k) by A241, FUNCT_1:def 3;

                  reconsider k as Element of NAT by A242;

                  per cases ;

                    suppose k = 1;

                    then

                     A244: (H . k) = ((G . 1) \/ (F . (n + 1))) by A194, A242;

                    per cases by A240, A243, A244, XBOOLE_0:def 3;

                      suppose

                       A245: v in (G . 1);

                      1 in ( dom G) by A221, FINSEQ_1:def 3;

                      then (G . 1) in ( rng G) by FUNCT_1: 3;

                      then v in ( union ( rng G)) by A245, TARSKI:def 4;

                      then v in ( dom f1) by A177, MESFUNC3:def 1;

                      then v in (( dom f) /\ ( union ( rng F1))) by RELAT_1: 61;

                      hence thesis by XBOOLE_0:def 4;

                    end;

                      suppose

                       A246: v in (F . (n + 1));

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

                      then (n + 1) in ( dom F) by A9, FINSEQ_3: 25;

                      then (F . (n + 1)) in ( rng F) by FUNCT_1: 3;

                      then v in ( union ( rng F)) by A246, TARSKI:def 4;

                      hence thesis by A6, MESFUNC3:def 1;

                    end;

                  end;

                    suppose

                     A247: k <> 1;

                    1 <= k by A194, A242, FINSEQ_1: 1;

                    then 1 < k by A247, XXREAL_0: 1;

                    then (1 + 1) <= k by NAT_1: 13;

                    then

                     A248: v in (G . k) by A194, A240, A242, A243;

                    k in ( dom G) by A194, A242, FINSEQ_1:def 3;

                    then (G . k) in ( rng G) by FUNCT_1: 3;

                    then v in ( union ( rng G)) by A248, TARSKI:def 4;

                    then v in ( dom f1) by A177, MESFUNC3:def 1;

                    then v in (( dom f) /\ ( union ( rng F1))) by RELAT_1: 61;

                    hence thesis by XBOOLE_0:def 4;

                  end;

                end;

                 A249:

                now

                  assume -infty in ( rng x1);

                  then

                  consider l be object such that

                   A250: l in ( dom x1) and

                   A251: (x1 . l) = -infty by FUNCT_1:def 3;

                  reconsider l as Element of NAT by A250;

                  l in (( dom x) /\ ( Seg n)) by A250, RELAT_1: 61;

                  then

                   A252: l in ( dom x) by XBOOLE_0:def 4;

                  (x . l) = -infty by A250, A251, FUNCT_1: 47;

                  then

                   A253: ((a . l) * ((M * F) . l)) = -infty by A8, A252;

                  per cases ;

                    suppose

                     A254: (F . l) <> {} ;

                    reconsider EMPTY = {} as Element of S by MEASURE1: 7;

                    consider v be object such that

                     A255: v in (F . l) by A254, XBOOLE_0:def 1;

                    

                     A256: (F . l) in ( rng F) by A7, A252, FUNCT_1: 3;

                    then v in ( union ( rng F)) by A255, TARSKI:def 4;

                    then

                     A257: v in ( dom f) by A6, MESFUNC3:def 1;

                    ( rng F) c= S by FINSEQ_1:def 4;

                    then

                    reconsider Fl = (F . l) as Element of S by A256;

                    EMPTY c= (F . l);

                    then (M . {} ) <= (M . Fl) by MEASURE1: 31;

                    then 0. <= (M . Fl) by VALUED_0:def 19;

                    then

                     A258: 0. <= ((M * F) . l) by A7, A252, FUNCT_1: 13;

                    (a . l) = (f . v) by A6, A7, A252, A255, MESFUNC3:def 1;

                    then 0. <= (a . l) by A257, a5;

                    hence contradiction by A253, A258;

                  end;

                    suppose

                     A259: (F . l) = {} ;

                    ((M * F) . l) = (M . (F . l)) by A7, A252, FUNCT_1: 13

                    .= 0. by A259, VALUED_0:def 19;

                    hence contradiction by A253;

                  end;

                end;

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

                then

                 A260: (n + 1) in ( dom F) by A9, FINSEQ_3: 25;

                

                 A261: (x . (n + 1)) = 0.

                proof

                  per cases by A187;

                    suppose

                     A262: (F . (n + 1)) = {} ;

                    ((M * F) . (n + 1)) = (M . (F . (n + 1))) by A260, FUNCT_1: 13;

                    then

                     A263: ((M * F) . (n + 1)) = 0. by A262, VALUED_0:def 19;

                    (x . (n + 1)) = ((a . (n + 1)) * ((M * F) . (n + 1))) by A7, A8, A260;

                    hence thesis by A263;

                  end;

                    suppose

                     A264: (a . (n + 1)) = 0. ;

                    (x . (n + 1)) = ((a . (n + 1)) * ((M * F) . (n + 1))) by A7, A8, A260;

                    hence thesis by A264;

                  end;

                end;

                 A265:

                now

                  assume -infty in ( rng <*(x . (n + 1))*>);

                  then -infty in {(x . (n + 1))} by FINSEQ_1: 39;

                  hence contradiction by A261;

                end;

                

                 A266: for m be Nat st m in ( dom H) holds for x be object st x in (H . m) holds (f . x) = (b . m)

                proof

                  let m be Nat;

                  assume

                   A267: m in ( dom H);

                  let x be object;

                  assume

                   A268: x in (H . m);

                  per cases ;

                    suppose

                     A269: m = 1;

                    then

                     A270: (H . m) = ((G . 1) \/ (F . (n + 1))) by A194, A267;

                    per cases by A268, A270, XBOOLE_0:def 3;

                      suppose

                       A271: x in (G . 1);

                      

                       A272: m in ( dom G) by A194, A267, FINSEQ_1:def 3;

                      then (G . 1) in ( rng G) by A269, FUNCT_1: 3;

                      then x in ( union ( rng G)) by A271, TARSKI:def 4;

                      then

                       A273: x in ( dom f1) by A177, MESFUNC3:def 1;

                      (f1 . x) = (b . m) by A177, A269, A271, A272, MESFUNC3:def 1;

                      hence thesis by A273, FUNCT_1: 47;

                    end;

                      suppose

                       A274: x in (F . (n + 1));

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

                      then (n + 1) in ( dom F) by A9, FINSEQ_3: 25;

                      hence thesis by A6, A178, A187, A269, A274, MESFUNC3:def 1;

                    end;

                  end;

                    suppose

                     A275: m <> 1;

                    1 <= m by A267, FINSEQ_3: 25;

                    then 1 < m by A275, XXREAL_0: 1;

                    then (1 + 1) <= m by NAT_1: 13;

                    then

                     A276: (H . m) = (G . m) by A194, A267;

                    

                     A277: m in ( dom G) by A194, A267, FINSEQ_1:def 3;

                    then (G . m) in ( rng G) by FUNCT_1: 3;

                    then x in ( union ( rng G)) by A268, A276, TARSKI:def 4;

                    then

                     A278: x in ( dom f1) by A177, MESFUNC3:def 1;

                    (f1 . x) = (b . m) by A177, A268, A277, A276, MESFUNC3:def 1;

                    hence thesis by A278, FUNCT_1: 47;

                  end;

                end;

                

                 A279: ( dom z) = ( dom y) by A220, FINSEQ_3: 29;

                then

                 A280: ( dom z) = ( dom H) by A180, A194, FINSEQ_1:def 3;

                

                 A281: for k be Nat st k in ( dom z) holds (z . k) = (y . k)

                proof

                  let k be Nat;

                  assume

                   A282: k in ( dom z);

                  then

                   A283: (z . k) = ((b . k) * ((M * H) . k)) by A220;

                  

                   A284: (y . k) = ((b . k) * ((M * G) . k)) by A181, A279, A282;

                  per cases ;

                    suppose

                     A285: k = 1;

                    then (z . k) = 0. by A178, A283;

                    hence thesis by A178, A284, A285;

                  end;

                    suppose

                     A286: k <> 1;

                    

                     A287: k in ( Seg ( len G)) by A180, A279, A282, FINSEQ_1:def 3;

                    then 1 <= k by FINSEQ_1: 1;

                    then 1 < k by A286, XXREAL_0: 1;

                    then

                     A288: (1 + 1) <= k by NAT_1: 13;

                    ((M * H) . k) = (M . (H . k)) by A280, A282, FUNCT_1: 13

                    .= (M . (G . k)) by A194, A287, A288

                    .= ((M * G) . k) by A180, A279, A282, FUNCT_1: 13;

                    hence thesis by A181, A279, A282, A283;

                  end;

                end;

                ( len x) = (n + 1) by A7, A9, FINSEQ_3: 29;

                

                then x = (x | (n + 1)) by FINSEQ_1: 58

                .= (x | ( Seg (n + 1))) by FINSEQ_1:def 15

                .= (x1 ^ <*(x . (n + 1))*>) by A7, A260, FINSEQ_5: 10;

                

                then

                 A289: ( Sum x) = (( Sum x1) + ( Sum <*(x . (n + 1))*>)) by A249, A265, EXTREAL1: 10

                .= (( Sum x1) + 0. ) by A261, EXTREAL1: 8;

                ( dom H) = ( dom G) by A194, FINSEQ_1:def 3

                .= ( dom b) by A177, MESFUNC3:def 1;

                then (H,b) are_Re-presentation_of f by A222, A266, MESFUNC3:def 1;

                

                then ( integral (M,f)) = ( Sum z) by A3, A5, A178, A179, A220, A280, MESFUNC3:def 2

                .= ( integral (M,f1)) by A182, A279, A281, FINSEQ_1: 13

                .= ( Sum x1) by A2, A23, A28, A14, A172, A183, A176, a12

                .= ( Sum x) by A289, XXREAL_3: 4;

                hence thesis;

              end;

                case

                 A290: (F . (n + 1)) <> {} & (a . (n + 1)) <> 0. ;

                defpred Pc[ Nat, set] means ($1 <= ( len b) implies $2 = (b . $1)) & ($1 = (( len b) + 1) implies $2 = (a . (n + 1)));

                

                 A291: f is real-valued by A3, MESFUNC2:def 4;

                consider v be object such that

                 A292: v in (F . (n + 1)) by A290, XBOOLE_0:def 1;

                

                 A293: for k be Nat st k in ( Seg (( len b) + 1)) holds ex v be Element of ExtREAL st Pc[k, v]

                proof

                  let k be Nat;

                  assume k in ( Seg (( len b) + 1));

                  per cases ;

                    suppose

                     A294: k <> (( len b) + 1);

                    reconsider v = (b . k) as Element of ExtREAL ;

                    take v;

                    thus thesis by A294;

                  end;

                    suppose

                     A295: k = (( len b) + 1);

                    reconsider v = (a . (n + 1)) as Element of ExtREAL ;

                    take v;

                    thus thesis by A295, NAT_1: 13;

                  end;

                end;

                consider c be FinSequence of ExtREAL such that

                 A296: ( dom c) = ( Seg (( len b) + 1)) & for k be Nat st k in ( Seg (( len b) + 1)) holds Pc[k, (c . k)] from FINSEQ_1:sch 5( A293);

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

                then

                 A297: (n + 1) in ( dom F) by A9, FINSEQ_3: 25;

                then (F . (n + 1)) in ( rng F) by FUNCT_1: 3;

                then v in ( union ( rng F)) by A292, TARSKI:def 4;

                then

                 A298: v in ( dom f) by A6, MESFUNC3:def 1;

                ( dom f) c= X by RELAT_1:def 18;

                then

                reconsider v as Element of X by A298;

                (f . v) = (a . (n + 1)) by A6, A297, A292, MESFUNC3:def 1;

                then |.(a . (n + 1)).| < +infty by A291, A298, MESFUNC2:def 1;

                then

                 A299: (a . (n + 1)) < +infty by EXTREAL1: 21;

                

                 A300: ( len c) = (( len b) + 1) by A296, FINSEQ_1:def 3;

                

                 A301: 0. <= (f . v) by A298, a5;

                then

                 A302: 0. < (a . (n + 1)) by A6, A290, A297, A292, MESFUNC3:def 1;

                

                 A303: for m be Nat st 2 <= m & m in ( dom c) holds 0. < (c . m) & (c . m) < +infty

                proof

                  let m be Nat;

                  assume that

                   A304: 2 <= m and

                   A305: m in ( dom c);

                  

                   A306: m <= ( len c) by A305, FINSEQ_3: 25;

                  per cases ;

                    suppose m = ( len c);

                    hence thesis by A302, A299, A296, A300, A305;

                  end;

                    suppose m <> ( len c);

                    then m < (( len b) + 1) by A300, A306, XXREAL_0: 1;

                    then

                     A307: m <= ( len b) by NAT_1: 13;

                    1 <= m by A304, XXREAL_0: 2;

                    then

                     A308: m in ( dom b) by A307, FINSEQ_3: 25;

                    (c . m) = (b . m) by A296, A305, A307;

                    hence thesis by A179, A304, A308;

                  end;

                end;

                

                 A309: 0. <= (a . (n + 1)) by A6, A297, A292, A301, MESFUNC3:def 1;

                 A310:

                now

                  assume

                   A311: -infty in ( rng y) or -infty in ( rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*>);

                  per cases by A311;

                    suppose -infty in ( rng y);

                    then

                    consider k be object such that

                     A312: k in ( dom y) and

                     A313: -infty = (y . k) by FUNCT_1:def 3;

                    reconsider k as Element of NAT by A312;

                    

                     A314: (y . k) = ((b . k) * ((M * G) . k)) by A181, A312;

                    k in ( Seg ( len y)) by A312, FINSEQ_1:def 3;

                    then

                     A315: 1 <= k by FINSEQ_1: 1;

                    per cases ;

                      suppose k = 1;

                      hence contradiction by A178, A313, A314;

                    end;

                      suppose k <> 1;

                      then 1 < k by A315, XXREAL_0: 1;

                      then

                       A316: (1 + 1) <= k by NAT_1: 13;

                      k in ( dom b) by A177, A180, A312, MESFUNC3:def 1;

                      then

                       A317: 0. < (b . k) by A179, A316;

                      (G . k) in ( rng G) & ( rng G) c= S by A180, A312, FINSEQ_1:def 4, FUNCT_1: 3;

                      then

                      reconsider Gk = (G . k) as Element of S;

                      reconsider EMPTY = {} as Element of S by PROB_1: 4;

                      (M . EMPTY) <= (M . Gk) by MEASURE1: 31, XBOOLE_1: 2;

                      then

                       A318: 0. <= (M . Gk) by VALUED_0:def 19;

                      ((M * G) . k) = (M . (G . k)) by A180, A312, FUNCT_1: 13;

                      hence contradiction by A313, A314, A317, A318;

                    end;

                  end;

                    suppose

                     A319: -infty in ( rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*>);

                    reconsider EMPTY = {} as Element of S by PROB_1: 4;

                    

                     A320: ( rng F) c= S by FINSEQ_1:def 4;

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

                    then

                     A321: (n + 1) in ( dom F) by A9, FINSEQ_3: 25;

                    then (F . (n + 1)) in ( rng F) by FUNCT_1: 3;

                    then

                    reconsider Fn1 = (F . (n + 1)) as Element of S by A320;

                    

                     A322: ((M * F) . (n + 1)) = (M . Fn1) by A321, FUNCT_1: 13;

                    (M . EMPTY) <= (M . Fn1) by MEASURE1: 31, XBOOLE_1: 2;

                    then

                     A323: 0. <= (M . Fn1) by VALUED_0:def 19;

                     -infty in {((a . (n + 1)) * ((M * F) . (n + 1)))} by A319, FINSEQ_1: 38;

                    hence contradiction by A309, A323, A322, TARSKI:def 1;

                  end;

                end;

                

                 A324: not -infty in ( rng x1)

                proof

                  reconsider EMPTY = {} as Element of S by PROB_1: 4;

                  assume -infty in ( rng x1);

                  then

                  consider k be object such that

                   A325: k in ( dom x1) and

                   A326: -infty = (x1 . k) by FUNCT_1:def 3;

                  reconsider k as Element of NAT by A325;

                  k in (( dom x) /\ ( Seg n)) by A325, RELAT_1: 61;

                  then

                   A327: k in ( dom x) by XBOOLE_0:def 4;

                  then

                   A328: (x . k) = ((a . k) * ((M * F) . k)) by A8;

                  

                   A329: (F . k) in ( rng F) by A7, A327, FUNCT_1: 3;

                  ( rng F) c= S by FINSEQ_1:def 4;

                  then

                  reconsider Fk = (F . k) as Element of S by A329;

                  per cases ;

                    suppose (F . k) <> {} ;

                    then

                    consider v be object such that

                     A330: v in (F . k) by XBOOLE_0:def 1;

                    v in ( union ( rng F)) by A329, A330, TARSKI:def 4;

                    then

                     A331: v in ( dom f) by A6, MESFUNC3:def 1;

                    (a . k) = (f . v) by A6, A7, A327, A330, MESFUNC3:def 1;

                    then

                     A332: 0. <= (a . k) by A331, a5;

                    (M . EMPTY) <= (M . Fk) by MEASURE1: 31, XBOOLE_1: 2;

                    then

                     A333: 0. <= (M . Fk) by VALUED_0:def 19;

                    (M . Fk) = ((M * F) . k) by A7, A327, FUNCT_1: 13;

                    hence contradiction by A325, A326, A328, A332, A333, FUNCT_1: 47;

                  end;

                    suppose (F . k) = {} ;

                    

                    then 0. = (M . (F . k)) by VALUED_0:def 19

                    .= ((M * F) . k) by A7, A327, FUNCT_1: 13;

                    hence contradiction by A325, A326, A328, FUNCT_1: 47;

                  end;

                end;

                defpred PH[ Nat, set] means ($1 <= ( len G) implies $2 = (G . $1)) & ($1 = (( len G) + 1) implies $2 = (F . (n + 1)));

                

                 A334: ( dom G) = ( dom b) by A177, MESFUNC3:def 1;

                

                 A335: ( Seg ( len G)) = ( dom G) by FINSEQ_1:def 3

                .= ( Seg ( len b)) by A334, FINSEQ_1:def 3;

                then

                 A336: ( len G) = ( len b) by FINSEQ_1: 6;

                

                 A337: for k be Nat st k in ( Seg (( len G) + 1)) holds ex v be Element of S st PH[k, v]

                proof

                  let k be Nat;

                  assume

                   A338: k in ( Seg (( len G) + 1));

                  per cases ;

                    suppose

                     A339: k <> (( len G) + 1);

                    k <= (( len G) + 1) by A338, FINSEQ_1: 1;

                    then k < (( len G) + 1) by A339, XXREAL_0: 1;

                    then

                     A340: k <= ( len G) by NAT_1: 13;

                    1 <= k by A338, FINSEQ_1: 1;

                    then k in ( dom G) by A340, FINSEQ_3: 25;

                    then

                     A341: (G . k) in ( rng G) by FUNCT_1: 3;

                    ( rng G) c= S by FINSEQ_1:def 4;

                    then

                    reconsider v = (G . k) as Element of S by A341;

                    take v;

                    thus thesis by A339;

                  end;

                    suppose

                     A342: k = (( len G) + 1);

                    (F . (n + 1)) in ( rng F) & ( rng F) c= S by A297, FINSEQ_1:def 4, FUNCT_1: 3;

                    then

                    reconsider v = (F . (n + 1)) as Element of S;

                    take v;

                    thus thesis by A342, NAT_1: 13;

                  end;

                end;

                consider H be FinSequence of S such that

                 A343: ( dom H) = ( Seg (( len G) + 1)) & for k be Nat st k in ( Seg (( len G) + 1)) holds PH[k, (H . k)] from FINSEQ_1:sch 5( A337);

                

                 A344: for i,j be object st i <> j holds (H . i) misses (H . j)

                proof

                  let i,j be object;

                  assume

                   A345: i <> j;

                  per cases ;

                    suppose

                     A346: i in ( dom H) & j in ( dom H);

                    then

                    reconsider i, j as Element of NAT ;

                    

                     A347: 1 <= i by A343, A346, FINSEQ_1: 1;

                    

                     A348: j <= (( len G) + 1) by A343, A346, FINSEQ_1: 1;

                    

                     A349: for k be Nat st 1 <= k & k <= ( len G) holds (H . k) misses (F . (n + 1))

                    proof

                      

                       A350: ( union ( rng F1)) misses (F . (n + 1))

                      proof

                        assume ( union ( rng F1)) meets (F . (n + 1));

                        then

                        consider v be object such that

                         A351: v in ( union ( rng F1)) and

                         A352: v in (F . (n + 1)) by XBOOLE_0: 3;

                        consider A be set such that

                         A353: v in A and

                         A354: A in ( rng F1) by A351, TARSKI:def 4;

                        consider m be object such that

                         A355: m in ( dom F1) and

                         A356: A = (F1 . m) by A354, FUNCT_1:def 3;

                        reconsider m as Element of NAT by A355;

                        m in ( Seg ( len F1)) by A355, FINSEQ_1:def 3;

                        then m <= n by A176, FINSEQ_1: 1;

                        then

                         A357: m <> (n + 1) by NAT_1: 13;

                        (F1 . m) = (F . m) by A355, FUNCT_1: 47;

                        then A misses (F . (n + 1)) by A356, A357, PROB_2:def 2;

                        then (A /\ (F . (n + 1))) = {} ;

                        hence contradiction by A352, A353, XBOOLE_0:def 4;

                      end;

                      let k be Nat;

                      assume that

                       A358: 1 <= k and

                       A359: k <= ( len G);

                      k in ( dom G) by A358, A359, FINSEQ_3: 25;

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

                      then (G . k) c= ( dom f1) by A177, MESFUNC3:def 1;

                      then

                       A360: (G . k) c= (( dom f) /\ ( union ( rng F1))) by RELAT_1: 61;

                      k <= (( len G) + 1) by A359, NAT_1: 12;

                      then k in ( Seg (( len G) + 1)) by A358, FINSEQ_1: 1;

                      then (H . k) = (G . k) by A343, A359;

                      hence thesis by A360, A350, XBOOLE_1: 18, XBOOLE_1: 63;

                    end;

                    

                     A361: 1 <= j by A343, A346, FINSEQ_1: 1;

                    

                     A362: i <= (( len G) + 1) by A343, A346, FINSEQ_1: 1;

                    

                     A363: PH[i, (H . i)] by A343, A346;

                    

                     A364: PH[j, (H . j)] by A343, A346;

                    per cases ;

                      suppose

                       A365: i = (( len G) + 1);

                      then j < (( len G) + 1) by A345, A348, XXREAL_0: 1;

                      then j <= ( len G) by NAT_1: 13;

                      hence thesis by A361, A363, A349, A365;

                    end;

                      suppose i <> (( len G) + 1);

                      then

                       A366: i < (( len G) + 1) by A362, XXREAL_0: 1;

                      then

                       A367: i <= ( len G) by NAT_1: 13;

                      per cases ;

                        suppose j = (( len G) + 1);

                        hence thesis by A347, A364, A349, A367;

                      end;

                        suppose j <> (( len G) + 1);

                        then j < (( len G) + 1) by A348, XXREAL_0: 1;

                        hence thesis by A345, A363, A364, A366, NAT_1: 13, PROB_2:def 2;

                      end;

                    end;

                  end;

                    suppose

                     A368: not i in ( dom H) or not j in ( dom H);

                    per cases by A368;

                      suppose not i in ( dom H);

                      then (H . i) = {} by FUNCT_1:def 2;

                      hence thesis;

                    end;

                      suppose not j in ( dom H);

                      then (H . j) = {} by FUNCT_1:def 2;

                      hence thesis;

                    end;

                  end;

                end;

                

                 A369: ( len H) = (( len G) + 1) by A343, FINSEQ_1:def 3;

                

                 A370: ( Seg ( len H)) = ( Seg (( len G) + 1)) by A343, FINSEQ_1:def 3;

                defpred Pz[ Nat, set] means ($1 <= ( len y) implies $2 = ((b . $1) * ((M * H) . $1))) & ($1 = (( len y) + 1) implies $2 = ((a . (n + 1)) * ((M * F) . (n + 1))));

                

                 A371: for k be Nat st k in ( Seg (( len y) + 1)) holds ex v be Element of ExtREAL st Pz[k, v]

                proof

                  let k be Nat;

                  assume k in ( Seg (( len y) + 1));

                  per cases ;

                    suppose

                     A372: k <> (( len y) + 1);

                    reconsider v = ((b . k) * ((M * H) . k)) as Element of ExtREAL ;

                    take v;

                    thus thesis by A372;

                  end;

                    suppose

                     A373: k = (( len y) + 1);

                    reconsider v = ((a . (n + 1)) * ((M * F) . (n + 1))) as Element of ExtREAL ;

                    take v;

                    thus thesis by A373, NAT_1: 13;

                  end;

                end;

                consider z be FinSequence of ExtREAL such that

                 A374: ( dom z) = ( Seg (( len y) + 1)) & for k be Nat st k in ( Seg (( len y) + 1)) holds Pz[k, (z . k)] from FINSEQ_1:sch 5( A371);

                

                 A375: ( len y) = ( len G) by A180, FINSEQ_3: 29;

                then

                 A376: ( len z) = (( len G) + 1) by A374, FINSEQ_1:def 3;

                then

                 A377: ( len z) in ( dom H) by A343, FINSEQ_1: 4;

                

                 A378: ( len z) in ( Seg (( len G) + 1)) by A376, FINSEQ_1: 4;

                

                 A379: ((M * F) . (n + 1)) = (M . (F . (n + 1))) by A174, FINSEQ_1: 4, FUNCT_1: 13

                .= (M . (H . ( len z))) by A343, A376, A378

                .= ((M * H) . ( len z)) by A377, FUNCT_1: 13;

                

                 A380: for m be Nat st m in ( dom z) holds (z . m) = ((c . m) * ((M * H) . m))

                proof

                  let m be Nat;

                  assume

                   A381: m in ( dom z);

                  then

                   A382: Pc[m, (c . m)] by A296, A336, A374, A375;

                  per cases ;

                    suppose m = (( len y) + 1);

                    hence thesis by A335, A374, A375, A376, A379, A381, A382, FINSEQ_1: 6;

                  end;

                    suppose

                     A383: m <> (( len y) + 1);

                    m <= (( len y) + 1) by A374, A381, FINSEQ_1: 1;

                    then m < (( len y) + 1) by A383, XXREAL_0: 1;

                    then

                     A384: m <= ( len b) by A336, A375, NAT_1: 13;

                    then (c . m) = (b . m) by A296, A336, A374, A375, A381;

                    hence thesis by A336, A374, A375, A381, A384;

                  end;

                end;

                reconsider H as Finite_Sep_Sequence of S by A344, PROB_2:def 2;

                

                 A385: ( len G) = ( len y) by A180, FINSEQ_3: 29;

                

                 A386: ( len z) = (( len y) + 1) by A374, FINSEQ_1:def 3;

                then ( len z) in ( Seg (( len y) + 1)) by FINSEQ_1: 4;

                then

                 A387: (z . ( len z)) = ((a . (n + 1)) * ((M * F) . (n + 1))) by A374, A386;

                

                 A388: for k be Nat st 1 <= k & k <= ( len z) holds (z . k) = ((y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k)

                proof

                  let k be Nat;

                  assume that

                   A389: 1 <= k and

                   A390: k <= ( len z);

                  per cases ;

                    suppose k = ( len z);

                    hence thesis by A386, A387, FINSEQ_1: 42;

                  end;

                    suppose k <> ( len z);

                    then k < ( len z) by A390, XXREAL_0: 1;

                    then

                     A391: k <= ( len y) by A386, NAT_1: 13;

                    then

                     A392: k in ( dom y) by A389, FINSEQ_3: 25;

                    

                    then

                     A393: ((y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k) = (y . k) by FINSEQ_1:def 7

                    .= ((b . k) * ((M * G) . k)) by A181, A392

                    .= ((b . k) * (M . (G . k))) by A180, A392, FUNCT_1: 13;

                    

                     A394: k in ( Seg ( len z)) by A389, A390, FINSEQ_1: 1;

                    then

                     A395: (M . (H . k)) = ((M * H) . k) by A343, A385, A386, FUNCT_1: 13;

                    (H . k) = (G . k) by A343, A385, A386, A391, A394;

                    hence thesis by A374, A386, A391, A393, A394, A395;

                  end;

                end;

                ( len (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>)) = (( len y) + 1) by FINSEQ_2: 16

                .= ( len z) by A374, FINSEQ_1:def 3;

                then

                 A396: z = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) by A388, FINSEQ_1: 14;

                ( len x) = (n + 1) by A7, A9, FINSEQ_3: 29;

                

                then

                 A397: x = (x | (n + 1)) by FINSEQ_1: 58

                .= (x | ( Seg (n + 1))) by FINSEQ_1:def 15

                .= (x1 ^ <*(x . (n + 1))*>) by A7, A297, FINSEQ_5: 10

                .= (x1 ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) by A7, A8, A297;

                ( dom G) <> {}

                proof

                  assume ( dom G) = {} ;

                  

                  then {} = ( union ( rng G)) by RELAT_1: 42, ZFMISC_1: 2

                  .= ( dom f1) by A177, MESFUNC3:def 1;

                  hence contradiction by A172;

                end;

                then b <> {} by A177, MESFUNC3:def 1, RELAT_1: 38;

                then ( len b) in ( Seg ( len b)) by FINSEQ_1: 3;

                then

                 A398: 1 <= ( len b) by FINSEQ_1: 1;

                

                 A399: for k be Nat st 1 <= k & k <= ( len H) holds (H . k) = ((G ^ <*(F . (n + 1))*>) . k)

                proof

                  let k be Nat;

                  assume that

                   A400: 1 <= k and

                   A401: k <= ( len H);

                  k in ( Seg (( len G) + 1)) by A370, A400, A401, FINSEQ_1: 1;

                  then

                   A402: PH[k, (H . k)] by A343;

                  per cases ;

                    suppose k = (( len G) + 1);

                    hence thesis by A402, FINSEQ_1: 42;

                  end;

                    suppose k <> (( len G) + 1);

                    then

                     A403: k < (( len G) + 1) by A369, A401, XXREAL_0: 1;

                    then k <= ( len G) by NAT_1: 13;

                    then k in ( dom G) by A400, FINSEQ_3: 25;

                    hence thesis by A402, A403, FINSEQ_1:def 7, NAT_1: 13;

                  end;

                end;

                ( len H) = (( len G) + 1) by A343, FINSEQ_1:def 3

                .= (( len G) + ( len <*(F . (n + 1))*>)) by FINSEQ_1: 39

                .= ( len (G ^ <*(F . (n + 1))*>)) by FINSEQ_1: 22;

                then H = (G ^ <*(F . (n + 1))*>) by A399, FINSEQ_1: 14;

                

                then

                 A404: ( rng H) = (( rng G) \/ ( rng <*(F . (n + 1))*>)) by FINSEQ_1: 31

                .= (( rng G) \/ {(F . (n + 1))}) by FINSEQ_1: 38;

                (F | ( Seg (n + 1))) = (F1 ^ <*(F . (n + 1))*>) by A174, FINSEQ_1: 4, FINSEQ_5: 10;

                

                then (F1 ^ <*(F . (n + 1))*>) = (F | (n + 1)) by FINSEQ_1:def 15

                .= F by A9, FINSEQ_1: 58;

                

                then ( rng F) = (( rng F1) \/ ( rng <*(F . (n + 1))*>)) by FINSEQ_1: 31

                .= (( rng F1) \/ {(F . (n + 1))}) by FINSEQ_1: 38;

                

                then

                 A405: ( dom f) = ( union (( rng F1) \/ {(F . (n + 1))})) by A6, MESFUNC3:def 1

                .= (( dom f1) \/ ( union {(F . (n + 1))})) by A16, ZFMISC_1: 78

                .= (( union ( rng G)) \/ ( union {(F . (n + 1))})) by A177, MESFUNC3:def 1

                .= ( union ( rng H)) by A404, ZFMISC_1: 78;

                for m be Nat st m in ( dom H) holds for v be object st v in (H . m) holds (f . v) = (c . m)

                proof

                  let m be Nat;

                  assume

                   A406: m in ( dom H);

                  then

                   A407: PH[m, (H . m)] by A343;

                  

                   A408: m <= (( len G) + 1) by A343, A406, FINSEQ_1: 1;

                  let v be object;

                  assume

                   A409: v in (H . m);

                  

                   A410: Pc[m, (c . m)] by A343, A296, A336, A406;

                  

                   A411: 1 <= m by A343, A406, FINSEQ_1: 1;

                  per cases ;

                    suppose

                     A412: m = (( len G) + 1);

                    (n + 1) in ( dom F) by A174, FINSEQ_1: 4;

                    hence thesis by A6, A335, A407, A410, A409, A412, FINSEQ_1: 6, MESFUNC3:def 1;

                  end;

                    suppose m <> (( len G) + 1);

                    then

                     A413: m < (( len G) + 1) by A408, XXREAL_0: 1;

                    then

                     A414: m <= ( len G) by NAT_1: 13;

                    then m in ( Seg ( len G)) by A411, FINSEQ_1: 1;

                    then m in ( dom G) by FINSEQ_1:def 3;

                    then

                     A415: (G . m) in ( rng G) by FUNCT_1: 3;

                    (H . m) in ( rng H) by A406, FUNCT_1: 3;

                    then

                     A416: v in ( dom f) by A405, A409, TARSKI:def 4;

                    ( union ( rng G)) = ( union ( rng F1)) by A16, A177, MESFUNC3:def 1;

                    then v in ( union ( rng F1)) by A407, A409, A413, A415, NAT_1: 13, TARSKI:def 4;

                    then v in (( dom f) /\ ( union ( rng F1))) by A416, XBOOLE_0:def 4;

                    then

                     A417: v in ( dom f1) by RELAT_1: 61;

                    m in ( Seg ( len G)) by A411, A414, FINSEQ_1: 1;

                    then m in ( dom G) by FINSEQ_1:def 3;

                    then (f1 . v) = (c . m) by A177, A336, A407, A410, A409, A413, MESFUNC3:def 1, NAT_1: 13;

                    hence thesis by A417, FUNCT_1: 47;

                  end;

                end;

                then

                 A418: (H,c) are_Re-presentation_of f by A343, A296, A336, A405, MESFUNC3:def 1;

                1 <= (( len b) + 1) by NAT_1: 11;

                then 1 in ( Seg (( len b) + 1)) by FINSEQ_1: 1;

                then (c . 1) = 0. by A178, A296, A398;

                

                then ( integral (M,f)) = ( Sum z) by A3, A5, A343, A303, A374, A375, A380, A418, MESFUNC3:def 2

                .= (( Sum y) + ( Sum <*((a . (n + 1)) * ((M * H) . ( len z)))*>)) by A379, A310, A396, EXTREAL1: 10

                .= (( integral (M,f1)) + ((a . (n + 1)) * ((M * H) . ( len z)))) by A182, EXTREAL1: 8

                .= (( Sum x1) + ((a . (n + 1)) * ((M * F) . (n + 1)))) by A2, A23, A28, A14, A172, A183, A176, A379, a12

                .= (( Sum x1) + ( Sum <*((a . (n + 1)) * ((M * F) . (n + 1)))*>)) by EXTREAL1: 8

                .= ( Sum x) by A310, A324, A397, EXTREAL1: 10;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A419: P[ 0 ]

      proof

        let f be PartFunc of X, ExtREAL ;

        let F be Finite_Sep_Sequence of S;

        let a,x be FinSequence of ExtREAL ;

        assume that f is_simple_func_in S and

         A420: ( dom f) <> {} and f is nonnegative and

         A421: (F,a) are_Re-presentation_of f and ( dom x) = ( dom F) and for i be Nat st i in ( dom x) holds (x . i) = ((a . i) * ((M * F) . i)) and

         A422: ( len F) = 0 ;

        ( Seg ( len F)) = {} by A422;

        then ( dom F) = {} by FINSEQ_1:def 3;

        then ( union ( rng F)) = {} by RELAT_1: 42, ZFMISC_1: 2;

        hence thesis by A420, A421, MESFUNC3:def 1;

      end;

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

      hence thesis;

    end;

    theorem :: MESFUNC4:3

    

     Th3: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL , M be sigma_Measure of S, F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL st f is_simple_func_in S & ( dom f) <> {} & f is nonnegative & (F,a) are_Re-presentation_of f & ( dom x) = ( dom F) & (for n be Nat st n in ( dom x) holds (x . n) = ((a . n) * ((M * F) . n))) holds ( integral (M,f)) = ( Sum x)

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      let M be sigma_Measure of S;

      let F be Finite_Sep_Sequence of S;

      let a,x be FinSequence of ExtREAL ;

      

       A1: ( len F) = ( len F);

      assume f is_simple_func_in S & ( dom f) <> {} & f is nonnegative & (F,a) are_Re-presentation_of f & (( dom x) = ( dom F) & for n be Nat st n in ( dom x) holds (x . n) = ((a . n) * ((M * F) . n)));

      hence thesis by A1, Th2;

    end;

    theorem :: MESFUNC4:4

    

     Th4: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL , M be sigma_Measure of S st f is_simple_func_in S & ( dom f) <> {} & f is nonnegative holds ex F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL st (F,a) are_Re-presentation_of f & ( dom x) = ( dom F) & (for n be Nat st n in ( dom x) holds (x . n) = ((a . n) * ((M * F) . n))) & ( integral (M,f)) = ( Sum x)

    proof

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

      assume that

       A1: f is_simple_func_in S and

       A2: ( dom f) <> {} & f is nonnegative;

      consider F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL such that

       A3: (F,a) are_Re-presentation_of f by A1, MESFUNC3: 12;

      ex x be FinSequence of ExtREAL st ( dom x) = ( dom F) & for n be Nat st n in ( dom x) holds (x . n) = ((a . n) * ((M * F) . n))

      proof

        deffunc Q( Nat) = ((a . $1) * ((M * F) . $1));

        consider x be FinSequence of ExtREAL such that

         A4: ( len x) = ( len F) & for k be Nat st k in ( dom x) holds (x . k) = Q(k) from FINSEQ_2:sch 1;

        take x;

        ( dom x) = ( Seg ( len F)) by A4, FINSEQ_1:def 3

        .= ( dom F) by FINSEQ_1:def 3;

        hence thesis by A4;

      end;

      then

      consider x be FinSequence of ExtREAL such that

       A5: ( dom x) = ( dom F) & for n be Nat st n in ( dom x) holds (x . n) = ((a . n) * ((M * F) . n));

      ( integral (M,f)) = ( Sum x) by A1, A2, A3, A5, Th3;

      hence thesis by A3, A5;

    end;

    theorem :: MESFUNC4:5

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL st f is_simple_func_in S & ( dom f) <> {} & f is nonnegative & g is_simple_func_in S & ( dom g) = ( dom f) & g is nonnegative holds (f + g) is_simple_func_in S & ( dom (f + g)) <> {} & (for x be object st x in ( dom (f + g)) holds 0. <= ((f + g) . x)) & ( integral (M,(f + g))) = (( integral (M,f)) + ( integral (M,g)))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL such that

       A1: f is_simple_func_in S and

       A2: ( dom f) <> {} and

       A3: f is nonnegative and

       A4: g is_simple_func_in S and

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

       A6: g is nonnegative;

      

       A7: g is real-valued by A4, MESFUNC2:def 4;

      

      then

       A8: ( dom (f + g)) = (( dom f) /\ ( dom f)) by A5, MESFUNC2: 2

      .= ( dom f);

      consider G be Finite_Sep_Sequence of S, b,y be FinSequence of ExtREAL such that

       A9: (G,b) are_Re-presentation_of g and ( dom y) = ( dom G) and for n be Nat st n in ( dom y) holds (y . n) = ((b . n) * ((M * G) . n)) and ( integral (M,g)) = ( Sum y) by A2, A4, A5, A6, Th4;

      set lb = ( len b);

      consider F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL such that

       A10: (F,a) are_Re-presentation_of f and ( dom x) = ( dom F) and for n be Nat st n in ( dom x) holds (x . n) = ((a . n) * ((M * F) . n)) and ( integral (M,f)) = ( Sum x) by A1, A2, A3, Th4;

      deffunc B1( Nat) = (b . ((($1 -' 1) mod lb) + 1));

      deffunc A1( Nat) = (a . ((($1 -' 1) div lb) + 1));

      set la = ( len a);

      

       A11: ( dom F) = ( dom a) by A10, MESFUNC3:def 1;

      deffunc FG1( Nat) = ((F . ((($1 -' 1) div lb) + 1)) /\ (G . ((($1 -' 1) mod lb) + 1)));

      consider FG be FinSequence such that

       A12: ( len FG) = (la * lb) and

       A13: for k be Nat st k in ( dom FG) holds (FG . k) = FG1(k) from FINSEQ_1:sch 2;

      

       A14: ( dom FG) = ( Seg (la * lb)) by A12, FINSEQ_1:def 3;

      

       A15: ( dom G) = ( dom b) by A9, MESFUNC3:def 1;

      now

        reconsider la9 = la, lb9 = lb as Nat;

        let k be Nat;

        set i = (((k -' 1) div lb) + 1);

        set j = (((k -' 1) mod lb) + 1);

        assume

         A16: k in ( dom FG);

        then

         A17: k in ( Seg (la * lb)) by A12, FINSEQ_1:def 3;

        then

         A18: k <= (la * lb) by FINSEQ_1: 1;

        then (k -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

        then

         A19: ((k -' 1) div lb) <= (((la * lb) -' 1) div lb) by NAT_2: 24;

        1 <= k by A17, FINSEQ_1: 1;

        then

         A20: lb9 divides (la9 * lb9) & 1 <= (la * lb) by A18, NAT_D:def 3, XXREAL_0: 2;

        

         A21: lb <> 0 by A17;

        then lb >= ( 0 + 1) by NAT_1: 13;

        then (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A20, NAT_2: 15;

        then

         A22: (((k -' 1) div lb) + 1) <= ((la * lb) div lb) by A19, XREAL_1: 19;

        reconsider la, lb as Nat;

        i >= ( 0 + 1) & i <= la by A21, A22, NAT_D: 18, XREAL_1: 6;

        then i in ( Seg la) by FINSEQ_1: 1;

        then i in ( dom F) by A11, FINSEQ_1:def 3;

        then

         A23: (F . i) in ( rng F) by FUNCT_1: 3;

        ((k -' 1) mod lb) < lb by A21, NAT_D: 1;

        then j >= ( 0 + 1) & j <= lb by NAT_1: 13;

        then j in ( Seg lb) by FINSEQ_1: 1;

        then j in ( dom G) by A15, FINSEQ_1:def 3;

        then

         A24: (G . j) in ( rng G) by FUNCT_1: 3;

        ( rng F) c= S & ( rng G) c= S by FINSEQ_1:def 4;

        then ((F . i) /\ (G . j)) in S by A23, A24, MEASURE1: 34;

        hence (FG . k) in S by A13, A16;

      end;

      then

      reconsider FG as FinSequence of S by FINSEQ_2: 12;

      for k,l be Nat st k in ( dom FG) & l in ( dom FG) & k <> l holds (FG . k) misses (FG . l)

      proof

        reconsider la9 = la, lb9 = lb as Nat;

        let k,l be Nat;

        assume that

         A25: k in ( dom FG) and

         A26: l in ( dom FG) and

         A27: k <> l;

        

         A28: l in ( Seg (la * lb)) by A12, A26, FINSEQ_1:def 3;

        set m = (((l -' 1) mod lb) + 1);

        set n = (((l -' 1) div lb) + 1);

        set j = (((k -' 1) mod lb) + 1);

        set i = (((k -' 1) div lb) + 1);

        

         A29: (FG . k) = ((F . i) /\ (G . j)) by A13, A25;

        

         A30: k in ( Seg (la * lb)) by A12, A25, FINSEQ_1:def 3;

        then

         A31: k <= (la * lb) by FINSEQ_1: 1;

        

         A32: 1 <= k by A30, FINSEQ_1: 1;

        then

         A33: lb9 divides (la9 * lb9) & 1 <= (la * lb) by A31, NAT_D:def 3, XXREAL_0: 2;

        

         A34: lb <> 0 by A30;

        then lb >= ( 0 + 1) by NAT_1: 13;

        then

         A35: (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A33, NAT_2: 15;

        (k -' 1) <= ((la * lb) -' 1) by A31, NAT_D: 42;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A35, NAT_2: 24;

        then

         A36: (((k -' 1) div lb) + 1) <= ((la * lb) div lb) by XREAL_1: 19;

        reconsider la, lb as Nat;

        i >= ( 0 + 1) & i <= la by A34, A36, NAT_D: 18, XREAL_1: 6;

        then i in ( Seg la) by FINSEQ_1: 1;

        then

         A37: i in ( dom F) by A11, FINSEQ_1:def 3;

        

         A38: 1 <= l by A28, FINSEQ_1: 1;

        

         A39: i <> n or j <> m

        proof

          ((l -' 1) + 1) = ((((n - 1) * lb) + (m - 1)) + 1) by A34, NAT_D: 2;

          then

           A40: ((l - 1) + 1) = (((n - 1) * lb) + m) by A38, XREAL_1: 233;

          ((k -' 1) + 1) = ((((i - 1) * lb) + (j - 1)) + 1) by A34, NAT_D: 2;

          then

           A41: ((k - 1) + 1) = (((i - 1) * lb) + j) by A32, XREAL_1: 233;

          assume i = n & j = m;

          hence contradiction by A27, A41, A40;

        end;

        ((l -' 1) mod lb) < lb by A34, NAT_D: 1;

        then m >= ( 0 + 1) & m <= lb by NAT_1: 13;

        then m in ( Seg lb) by FINSEQ_1: 1;

        then

         A42: m in ( dom G) by A15, FINSEQ_1:def 3;

        ((k -' 1) mod lb) < lb by A34, NAT_D: 1;

        then j >= ( 0 + 1) & j <= lb by NAT_1: 13;

        then j in ( Seg lb) by FINSEQ_1: 1;

        then

         A43: j in ( dom G) by A15, FINSEQ_1:def 3;

        l <= (la * lb) by A28, FINSEQ_1: 1;

        then (l -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

        then ((l -' 1) div lb) <= (((la * lb) div lb) - 1) by A35, NAT_2: 24;

        then (((l -' 1) div lb) + 1) <= ((la * lb) div lb) by XREAL_1: 19;

        then n >= ( 0 + 1) & n <= la by A34, NAT_D: 18, XREAL_1: 6;

        then n in ( Seg la) by FINSEQ_1: 1;

        then

         A44: n in ( dom F) by A11, FINSEQ_1:def 3;

        per cases by A39;

          suppose i <> n;

          then

           A45: (F . i) misses (F . n) by A37, A44, MESFUNC3: 4;

          ((FG . k) /\ (FG . l)) = (((F . i) /\ (G . j)) /\ ((F . n) /\ (G . m))) by A13, A26, A29

          .= ((F . i) /\ ((G . j) /\ ((F . n) /\ (G . m)))) by XBOOLE_1: 16

          .= ((F . i) /\ ((F . n) /\ ((G . j) /\ (G . m)))) by XBOOLE_1: 16

          .= (((F . i) /\ (F . n)) /\ ((G . j) /\ (G . m))) by XBOOLE_1: 16

          .= ( {} /\ ((G . j) /\ (G . m))) by A45

          .= {} ;

          hence thesis;

        end;

          suppose j <> m;

          then

           A46: (G . j) misses (G . m) by A43, A42, MESFUNC3: 4;

          ((FG . k) /\ (FG . l)) = (((F . i) /\ (G . j)) /\ ((F . n) /\ (G . m))) by A13, A26, A29

          .= ((F . i) /\ ((G . j) /\ ((F . n) /\ (G . m)))) by XBOOLE_1: 16

          .= ((F . i) /\ ((F . n) /\ ((G . j) /\ (G . m)))) by XBOOLE_1: 16

          .= (((F . i) /\ (F . n)) /\ ((G . j) /\ (G . m))) by XBOOLE_1: 16

          .= (((F . i) /\ (F . n)) /\ {} ) by A46

          .= {} ;

          hence thesis;

        end;

      end;

      then

      reconsider FG as Finite_Sep_Sequence of S by MESFUNC3: 4;

      consider a1 be FinSequence of ExtREAL such that

       A47: ( len a1) = ( len FG) and

       A48: for k be Nat st k in ( dom a1) holds (a1 . k) = A1(k) from FINSEQ_2:sch 1;

      consider b1 be FinSequence of ExtREAL such that

       A49: ( len b1) = ( len FG) and

       A50: for k be Nat st k in ( dom b1) holds (b1 . k) = B1(k) from FINSEQ_2:sch 1;

      

       A51: ( dom f) = ( union ( rng F)) by A10, MESFUNC3:def 1;

      

       A52: ( dom a1) = ( Seg ( len FG)) by A47, FINSEQ_1:def 3;

      

       A53: for k be Nat st k in ( dom FG) holds for x be object st x in (FG . k) holds (f . x) = (a1 . k)

      proof

        reconsider la9 = la, lb9 = lb as Nat;

        let k be Nat;

        set i = (((k -' 1) div lb) + 1);

        assume

         A54: k in ( dom FG);

        then

         A55: k in ( Seg ( len FG)) by FINSEQ_1:def 3;

        

         A56: k in ( Seg ( len FG)) by A54, FINSEQ_1:def 3;

        then

         A57: k <= (la * lb) by A12, FINSEQ_1: 1;

        

         A58: lb <> 0 by A12, A56;

        then

         A59: lb >= ( 0 + 1) by NAT_1: 13;

        1 <= k by A56, FINSEQ_1: 1;

        then lb9 divides (la9 * lb9) & 1 <= (la * lb) by A57, NAT_D:def 3, XXREAL_0: 2;

        then

         A60: (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A59, NAT_2: 15;

        

         A61: ((la * lb) div lb) = la by A58, NAT_D: 18;

        (k -' 1) <= ((la * lb) -' 1) by A57, NAT_D: 42;

        then ((k -' 1) div lb) <= (((la * lb) -' 1) div lb) by NAT_2: 24;

        then i >= ( 0 + 1) & i <= ((la * lb) div lb) by A60, XREAL_1: 6, XREAL_1: 19;

        then i in ( Seg la) by A61, FINSEQ_1: 1;

        then

         A62: i in ( dom F) by A11, FINSEQ_1:def 3;

        let x be object;

        assume

         A63: x in (FG . k);

        (FG . k) = ((F . (((k -' 1) div lb) + 1)) /\ (G . (((k -' 1) mod lb) + 1))) by A13, A54;

        then x in (F . i) by A63, XBOOLE_0:def 4;

        

        hence (f . x) = (a . i) by A10, A62, MESFUNC3:def 1

        .= (a1 . k) by A48, A52, A55;

      end;

      

       A64: ( dom b1) = ( Seg ( len FG)) by A49, FINSEQ_1:def 3;

      

       A65: for k be Nat st k in ( dom FG) holds for x be object st x in (FG . k) holds (g . x) = (b1 . k)

      proof

        let k be Nat;

        set j = (((k -' 1) mod lb) + 1);

        assume

         A66: k in ( dom FG);

        then

         A67: k in ( Seg ( len FG)) by FINSEQ_1:def 3;

        k in ( Seg ( len FG)) by A66, FINSEQ_1:def 3;

        then lb <> 0 by A12;

        then ((k -' 1) mod lb) < lb by NAT_D: 1;

        then j >= ( 0 + 1) & j <= lb by NAT_1: 13;

        then j in ( Seg lb) by FINSEQ_1: 1;

        then

         A68: j in ( dom G) by A15, FINSEQ_1:def 3;

        let x be object;

        assume

         A69: x in (FG . k);

        (FG . k) = ((F . (((k -' 1) div lb) + 1)) /\ (G . (((k -' 1) mod lb) + 1))) by A13, A66;

        then x in (G . j) by A69, XBOOLE_0:def 4;

        

        hence (g . x) = (b . j) by A9, A68, MESFUNC3:def 1

        .= (b1 . k) by A50, A64, A67;

      end;

      

       A70: ( dom g) = ( union ( rng G)) by A9, MESFUNC3:def 1;

      

       A71: ( dom f) = ( union ( rng FG))

      proof

        thus ( dom f) c= ( union ( rng FG))

        proof

          let z be object;

          assume

           A72: z in ( dom f);

          then

          consider Y be set such that

           A73: z in Y and

           A74: Y in ( rng F) by A51, TARSKI:def 4;

          consider Z be set such that

           A75: z in Z and

           A76: Z in ( rng G) by A5, A70, A72, TARSKI:def 4;

          consider j be object such that

           A77: j in ( dom G) and

           A78: Z = (G . j) by A76, FUNCT_1:def 3;

          reconsider j as Element of NAT by A77;

          

           A79: j in ( Seg ( len b)) by A15, A77, FINSEQ_1:def 3;

          then

           A80: 1 <= j by FINSEQ_1: 1;

          then

          consider j9 be Nat such that

           A81: j = (1 + j9) by NAT_1: 10;

          consider i be object such that

           A82: i in ( dom F) and

           A83: Y = (F . i) by A74, FUNCT_1:def 3;

          reconsider i as Element of NAT by A82;

          

           A84: i in ( Seg ( len a)) by A11, A82, FINSEQ_1:def 3;

          then 1 <= i by FINSEQ_1: 1;

          then

          consider i9 be Nat such that

           A85: i = (1 + i9) by NAT_1: 10;

          

           A86: j <= lb by A79, FINSEQ_1: 1;

          then

           A87: j9 < lb by A81, NAT_1: 13;

          set k = (((i - 1) * lb) + j);

          reconsider k as Nat by A85;

          

           A88: k >= ( 0 + j) by A85, XREAL_1: 6;

          

          then

           A89: (k -' 1) = (k - 1) by A80, XREAL_1: 233, XXREAL_0: 2

          .= ((i9 * lb) + j9) by A85, A81;

          then

           A90: i = (((k -' 1) div lb) + 1) by A85, A87, NAT_D:def 1;

          i <= la by A84, FINSEQ_1: 1;

          then (i - 1) <= (la - 1) by XREAL_1: 9;

          then ((i - 1) * lb) <= ((la - 1) * lb) by XREAL_1: 64;

          then

           A91: k <= (((la - 1) * lb) + j) by XREAL_1: 6;

          (((la - 1) * lb) + j) <= (((la - 1) * lb) + lb) by A86, XREAL_1: 6;

          then

           A92: k <= (la * lb) by A91, XXREAL_0: 2;

          k >= 1 by A80, A88, XXREAL_0: 2;

          then

           A93: k in ( Seg (la * lb)) by A92, FINSEQ_1: 1;

          then k in ( dom FG) by A12, FINSEQ_1:def 3;

          then

           A94: (FG . k) in ( rng FG) by FUNCT_1:def 3;

          

           A95: j = (((k -' 1) mod lb) + 1) by A81, A89, A87, NAT_D:def 2;

          z in ((F . i) /\ (G . j)) by A73, A83, A75, A78, XBOOLE_0:def 4;

          then z in (FG . k) by A13, A14, A90, A95, A93;

          hence thesis by A94, TARSKI:def 4;

        end;

        reconsider la9 = la, lb9 = lb as Nat;

        let z be object;

        assume z in ( union ( rng FG));

        then

        consider Y be set such that

         A96: z in Y and

         A97: Y in ( rng FG) by TARSKI:def 4;

        consider k be object such that

         A98: k in ( dom FG) and

         A99: Y = (FG . k) by A97, FUNCT_1:def 3;

        reconsider k as Element of NAT by A98;

        set j = (((k -' 1) mod lb) + 1);

        set i = (((k -' 1) div lb) + 1);

        (FG . k) = ((F . i) /\ (G . j)) by A13, A98;

        then

         A100: z in (F . i) by A96, A99, XBOOLE_0:def 4;

        

         A101: k in ( Seg ( len FG)) by A98, FINSEQ_1:def 3;

        then

         A102: k <= (la * lb) by A12, FINSEQ_1: 1;

        

         A103: lb <> 0 by A12, A101;

        then

         A104: lb >= ( 0 + 1) by NAT_1: 13;

        1 <= k by A101, FINSEQ_1: 1;

        then lb9 divides (la9 * lb9) & 1 <= (la * lb) by A102, NAT_D:def 3, XXREAL_0: 2;

        then

         A105: (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A104, NAT_2: 15;

        reconsider i as Nat;

        

         A106: ((la * lb) div lb) = la by A103, NAT_D: 18;

        (k -' 1) <= ((la * lb) -' 1) by A102, NAT_D: 42;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A105, NAT_2: 24;

        then i >= ( 0 + 1) & i <= ((la * lb) div lb) by XREAL_1: 6, XREAL_1: 19;

        then i in ( Seg la) by A106, FINSEQ_1: 1;

        then i in ( dom F) by A11, FINSEQ_1:def 3;

        then (F . i) in ( rng F) by FUNCT_1:def 3;

        hence thesis by A51, A100, TARSKI:def 4;

      end;

      

       A107: for k be Nat, x,y be Element of X st k in ( dom FG) & x in (FG . k) & y in (FG . k) holds ((f + g) . x) = ((f + g) . y)

      proof

        reconsider la9 = la, lb9 = lb as Nat;

        let k be Nat;

        let x,y be Element of X;

        assume that

         A108: k in ( dom FG) and

         A109: x in (FG . k) and

         A110: y in (FG . k);

        set j = (((k -' 1) mod lb) + 1);

        

         A111: (FG . k) = ((F . (((k -' 1) div lb) + 1)) /\ (G . (((k -' 1) mod lb) + 1))) by A13, A108;

        then

         A112: x in (G . j) by A109, XBOOLE_0:def 4;

        set i = (((k -' 1) div lb) + 1);

        

         A113: k in ( Seg ( len FG)) by A108, FINSEQ_1:def 3;

        then

         A114: k <= (la * lb) by A12, FINSEQ_1: 1;

        then

         A115: (k -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

        1 <= k by A113, FINSEQ_1: 1;

        then

         A116: lb9 divides (la9 * lb9) & 1 <= (la * lb) by A114, NAT_D:def 3, XXREAL_0: 2;

        

         A117: lb <> 0 by A12, A113;

        then lb >= ( 0 + 1) by NAT_1: 13;

        then (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A116, NAT_2: 15;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A115, NAT_2: 24;

        then (((k -' 1) div lb) + 1) <= ((la * lb) div lb) by XREAL_1: 19;

        then i >= ( 0 + 1) & i <= la by A117, NAT_D: 18, XREAL_1: 6;

        then i in ( Seg la) by FINSEQ_1: 1;

        then

         A118: i in ( dom F) by A11, FINSEQ_1:def 3;

        x in (F . i) by A109, A111, XBOOLE_0:def 4;

        then

         A119: (f . x) = (a . i) by A10, A118, MESFUNC3:def 1;

        ((k -' 1) mod lb) < lb by A117, NAT_D: 1;

        then j >= ( 0 + 1) & j <= lb by NAT_1: 13;

        then j in ( Seg lb) by FINSEQ_1: 1;

        then

         A120: j in ( dom G) by A15, FINSEQ_1:def 3;

        y in (F . i) by A110, A111, XBOOLE_0:def 4;

        then

         A121: (f . y) = (a . i) by A10, A118, MESFUNC3:def 1;

        

         A122: y in (G . j) by A110, A111, XBOOLE_0:def 4;

        

         A123: (FG . k) in ( rng FG) by A108, FUNCT_1:def 3;

        then

         A124: y in ( dom (f + g)) by A71, A8, A110, TARSKI:def 4;

        x in ( dom (f + g)) by A71, A8, A109, A123, TARSKI:def 4;

        

        hence ((f + g) . x) = ((f . x) + (g . x)) by MESFUNC1:def 3

        .= ((a . i) + (b . j)) by A9, A120, A112, A119, MESFUNC3:def 1

        .= ((f . y) + (g . y)) by A9, A120, A122, A121, MESFUNC3:def 1

        .= ((f + g) . y) by A124, MESFUNC1:def 3;

      end;

      ex y1 be FinSequence of ExtREAL st ( dom y1) = ( dom FG) & for n be Nat st n in ( dom y1) holds (y1 . n) = ((b1 . n) * ((M * FG) . n))

      proof

        deffunc Y1( Nat) = ((b1 . $1) * ((M * FG) . $1));

        consider y1 be FinSequence of ExtREAL such that

         A125: ( len y1) = ( len FG) & for k be Nat st k in ( dom y1) holds (y1 . k) = Y1(k) from FINSEQ_2:sch 1;

        take y1;

        ( dom y1) = ( Seg ( len FG)) by A125, FINSEQ_1:def 3

        .= ( dom FG) by FINSEQ_1:def 3;

        hence thesis by A125;

      end;

      then

      consider y1 be FinSequence of ExtREAL such that

       A126: ( dom y1) = ( dom FG) and

       A127: for n be Nat st n in ( dom y1) holds (y1 . n) = ((b1 . n) * ((M * FG) . n));

      ex x1 be FinSequence of ExtREAL st ( dom x1) = ( dom FG) & for n be Nat st n in ( dom x1) holds (x1 . n) = ((a1 . n) * ((M * FG) . n))

      proof

        deffunc X1( Nat) = ((a1 . $1) * ((M * FG) . $1));

        consider x1 be FinSequence of ExtREAL such that

         A128: ( len x1) = ( len FG) & for k be Nat st k in ( dom x1) holds (x1 . k) = X1(k) from FINSEQ_2:sch 1;

        take x1;

        thus thesis by A128, FINSEQ_3: 29;

      end;

      then

      consider x1 be FinSequence of ExtREAL such that

       A129: ( dom x1) = ( dom FG) and

       A130: for n be Nat st n in ( dom x1) holds (x1 . n) = ((a1 . n) * ((M * FG) . n));

      ( dom FG) = ( Seg ( len a1)) by A47, FINSEQ_1:def 3

      .= ( dom a1) by FINSEQ_1:def 3;

      then (FG,a1) are_Re-presentation_of f by A71, A53, MESFUNC3:def 1;

      then

       A131: ( integral (M,f)) = ( Sum x1) by A1, A2, A3, A129, A130, Th3;

      deffunc C1( Nat) = ((a1 . $1) + (b1 . $1));

      consider c1 be FinSequence of ExtREAL such that

       A132: ( len c1) = ( len FG) and

       A133: for k be Nat st k in ( dom c1) holds (c1 . k) = C1(k) from FINSEQ_2:sch 1;

      ex z1 be FinSequence of ExtREAL st ( dom z1) = ( dom FG) & for n be Nat st n in ( dom z1) holds (z1 . n) = ((c1 . n) * ((M * FG) . n))

      proof

        deffunc Z1( Nat) = ((c1 . $1) * ((M * FG) . $1));

        consider z1 be FinSequence of ExtREAL such that

         A134: ( len z1) = ( len FG) & for k be Nat st k in ( dom z1) holds (z1 . k) = Z1(k) from FINSEQ_2:sch 1;

        take z1;

        thus thesis by A134, FINSEQ_3: 29;

      end;

      then

      consider z1 be FinSequence of ExtREAL such that

       A135: ( dom z1) = ( dom FG) and

       A136: for n be Nat st n in ( dom z1) holds (z1 . n) = ((c1 . n) * ((M * FG) . n));

      

       A137: ( dom c1) = ( Seg ( len FG)) by A132, FINSEQ_1:def 3;

      

       A138: for k be Nat st k in ( dom FG) holds for x be object st x in (FG . k) holds ((f + g) . x) = (c1 . k)

      proof

        let k be Nat;

        

         A139: ( dom (f + g)) c= X by RELAT_1:def 18;

        assume

         A140: k in ( dom FG);

        then

         A141: k in ( Seg ( len FG)) by FINSEQ_1:def 3;

        let x be object;

        assume

         A142: x in (FG . k);

        (FG . k) in ( rng FG) by A140, FUNCT_1:def 3;

        then x in ( dom (f + g)) by A71, A8, A142, TARSKI:def 4;

        

        hence ((f + g) . x) = ((f . x) + (g . x)) by A139, MESFUNC1:def 3

        .= ((a1 . k) + (g . x)) by A53, A140, A142

        .= ((a1 . k) + (b1 . k)) by A65, A140, A142

        .= (c1 . k) by A133, A137, A141;

      end;

      

       A143: for i be Nat st i in ( dom y1) holds 0. <= (y1 . i)

      proof

        let i be Nat;

        set i9 = (((i -' 1) mod lb) + 1);

        assume

         A144: i in ( dom y1);

        then

         A145: (y1 . i) = ((b1 . i) * ((M * FG) . i)) by A127;

        

         A146: i in ( Seg ( len FG)) by A126, A144, FINSEQ_1:def 3;

        then lb <> 0 by A12;

        then ((i -' 1) mod lb) < lb by NAT_D: 1;

        then i9 >= ( 0 + 1) & i9 <= lb by NAT_1: 13;

        then i9 in ( Seg lb) by FINSEQ_1: 1;

        then

         A147: i9 in ( dom G) by A15, FINSEQ_1:def 3;

        per cases ;

          suppose (G . i9) <> {} ;

          then

          consider x9 be object such that

           A148: x9 in (G . i9) by XBOOLE_0:def 1;

          (FG . i) in ( rng FG) & ( rng FG) c= S by A126, A144, FINSEQ_1:def 4, FUNCT_1: 3;

          then

          reconsider FGi = (FG . i) as Element of S;

          reconsider EMPTY = {} as Element of S by MEASURE1: 7;

          EMPTY c= FGi;

          then

           A149: (M . {} ) <= (M . FGi) by MEASURE1: 31;

          (g . x9) = (b . i9) by A9, A147, A148, MESFUNC3:def 1

          .= (b1 . i) by A50, A64, A146;

          then

           A151: 0. <= (b1 . i) by A6, SUPINF_2: 51;

          (M . {} ) = 0. by VALUED_0:def 19;

          then 0. <= ((M * FG) . i) by A126, A144, A149, FUNCT_1: 13;

          hence thesis by A145, A151;

        end;

          suppose

           A152: (G . i9) = {} ;

          (FG . i) = ((F . (((i -' 1) div lb) + 1)) /\ (G . i9)) by A13, A126, A144;

          then (M . (FG . i)) = 0. by A152, VALUED_0:def 19;

          then ((M * FG) . i) = 0. by A126, A144, FUNCT_1: 13;

          hence thesis by A145;

        end;

      end;

      then for i be object st i in ( dom y1) holds 0. <= (y1 . i);

      then

       Y: y1 is nonnegative by SUPINF_2: 52;

       not -infty in ( rng y1)

      proof

        assume -infty in ( rng y1);

        then ex i be object st i in ( dom y1) & (y1 . i) = -infty by FUNCT_1:def 3;

        hence contradiction by A143;

      end;

      

      then

       A153: ((x1 " { +infty }) /\ (y1 " { -infty })) = ((x1 " { +infty }) /\ {} ) by FUNCT_1: 72

      .= {} ;

      

       A154: for i be Nat st i in ( dom x1) holds 0. <= (x1 . i)

      proof

        reconsider la9 = la, lb9 = lb as Nat;

        let i be Nat;

        set i9 = (((i -' 1) div lb) + 1);

        assume

         A155: i in ( dom x1);

        then

         A156: (x1 . i) = ((a1 . i) * ((M * FG) . i)) by A130;

        

         A157: i in ( Seg ( len FG)) by A129, A155, FINSEQ_1:def 3;

        then

         A158: i <= (la * lb) by A12, FINSEQ_1: 1;

        

         A159: lb <> 0 by A12, A157;

        then

         A160: lb >= ( 0 + 1) by NAT_1: 13;

        1 <= i by A157, FINSEQ_1: 1;

        then lb9 divides (la9 * lb9) & 1 <= (la * lb) by A158, NAT_D:def 3, XXREAL_0: 2;

        then

         A161: (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A160, NAT_2: 15;

        (i -' 1) <= ((la * lb) -' 1) by A158, NAT_D: 42;

        then ((i -' 1) div lb) <= (((la * lb) div lb) - 1) by A161, NAT_2: 24;

        then

         A162: i9 >= ( 0 + 1) & i9 <= ((la * lb) div lb) by XREAL_1: 6, XREAL_1: 19;

        ((la * lb) div lb) = la by A159, NAT_D: 18;

        then i9 in ( Seg la) by A162, FINSEQ_1: 1;

        then

         A163: i9 in ( dom F) by A11, FINSEQ_1:def 3;

        per cases ;

          suppose (F . i9) <> {} ;

          then

          consider x9 be object such that

           A164: x9 in (F . i9) by XBOOLE_0:def 1;

          (FG . i) in ( rng FG) & ( rng FG) c= S by A129, A155, FINSEQ_1:def 4, FUNCT_1: 3;

          then

          reconsider FGi = (FG . i) as Element of S;

          reconsider EMPTY = {} as Element of S by MEASURE1: 7;

          EMPTY c= FGi;

          then

           A165: (M . {} ) <= (M . FGi) by MEASURE1: 31;

          (f . x9) = (a . i9) by A10, A163, A164, MESFUNC3:def 1

          .= (a1 . i) by A48, A52, A157;

          then

           A167: 0. <= (a1 . i) by A3, SUPINF_2: 51;

          (M . {} ) = 0. by VALUED_0:def 19;

          then 0. <= ((M * FG) . i) by A129, A155, A165, FUNCT_1: 13;

          hence thesis by A156, A167;

        end;

          suppose

           A168: (F . i9) = {} ;

          (FG . i) = ((F . i9) /\ (G . (((i -' 1) mod lb) + 1))) by A13, A129, A155;

          then (M . (FG . i)) = 0. by A168, VALUED_0:def 19;

          then ((M * FG) . i) = 0. by A129, A155, FUNCT_1: 13;

          hence thesis by A156;

        end;

      end;

      then for i be object st i in ( dom x1) holds 0. <= (x1 . i);

      then

       Z: x1 is nonnegative by SUPINF_2: 52;

       not -infty in ( rng x1)

      proof

        assume -infty in ( rng x1);

        then ex i be object st i in ( dom x1) & (x1 . i) = -infty by FUNCT_1:def 3;

        hence contradiction by A154;

      end;

      

      then ((x1 " { -infty }) /\ (y1 " { +infty })) = ( {} /\ (y1 " { +infty })) by FUNCT_1: 72

      .= {} ;

      

      then

       A169: ( dom (x1 + y1)) = ((( dom x1) /\ ( dom y1)) \ ( {} \/ {} )) by A153, MESFUNC1:def 3

      .= ( dom z1) by A129, A126, A135;

      

       A170: for k be Nat st k in ( dom z1) holds (z1 . k) = ((x1 + y1) . k)

      proof

        reconsider la9 = la, lb9 = lb as Nat;

        let k be Nat;

        set p = (((k -' 1) div lb) + 1);

        set q = (((k -' 1) mod lb) + 1);

        assume

         A171: k in ( dom z1);

        then

         A172: k in ( Seg ( len FG)) by A135, FINSEQ_1:def 3;

        then

         A173: k <= (la * lb) by A12, FINSEQ_1: 1;

        then

         A174: (k -' 1) <= ((la * lb) -' 1) by NAT_D: 42;

        1 <= k by A172, FINSEQ_1: 1;

        then

         A175: lb9 divides (la9 * lb9) & 1 <= (la * lb) by A173, NAT_D:def 3, XXREAL_0: 2;

        

         A176: lb <> 0 by A12, A172;

        then lb >= ( 0 + 1) by NAT_1: 13;

        then (((la9 * lb9) -' 1) div lb9) = (((la9 * lb9) div lb9) - 1) by A175, NAT_2: 15;

        then ((k -' 1) div lb) <= (((la * lb) div lb) - 1) by A174, NAT_2: 24;

        then p <= ((la * lb) div lb) by XREAL_1: 19;

        then p >= ( 0 + 1) & p <= la by A176, NAT_D: 18, XREAL_1: 6;

        then p in ( Seg la) by FINSEQ_1: 1;

        then

         A177: p in ( dom F) by A11, FINSEQ_1:def 3;

        ((k -' 1) mod lb) < lb by A176, NAT_D: 1;

        then q >= ( 0 + 1) & q <= lb by NAT_1: 13;

        then q in ( Seg lb) by FINSEQ_1: 1;

        then

         A178: q in ( dom G) by A15, FINSEQ_1:def 3;

        

         A179: (((a1 . k) + (b1 . k)) * ((M * FG) . k)) = (((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)))

        proof

          per cases ;

            suppose (FG . k) <> {} ;

            then ((F . p) /\ (G . q)) <> {} by A13, A135, A171;

            then

            consider v be object such that

             A180: v in ((F . p) /\ (G . q)) by XBOOLE_0:def 1;

            

             A181: v in (G . q) by A180, XBOOLE_0:def 4;

            (b . q) = (g . v) by A9, A178, A181, MESFUNC3:def 1;

            then 0. <= (b . q) by A6, SUPINF_2: 51;

            then

             A183: 0. = (b1 . k) or 0. < (b1 . k) by A50, A64, A172;

            

             A184: v in (F . p) by A180, XBOOLE_0:def 4;

            (a . p) = (f . v) by A10, A177, A184, MESFUNC3:def 1;

            then 0. <= (a . p) by A3, SUPINF_2: 51;

            then 0. = (a1 . k) or 0. < (a1 . k) by A48, A52, A172;

            hence thesis by A183, XXREAL_3: 96;

          end;

            suppose (FG . k) = {} ;

            then (M . (FG . k)) = 0. by VALUED_0:def 19;

            then

             A186: ((M * FG) . k) = 0. by A135, A171, FUNCT_1: 13;

            

            hence (((a1 . k) + (b1 . k)) * ((M * FG) . k)) = 0

            .= (((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))) by A186;

          end;

        end;

        

        thus (z1 . k) = ((c1 . k) * ((M * FG) . k)) by A136, A171

        .= (((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k))) by A133, A137, A172, A179

        .= ((x1 . k) + ((b1 . k) * ((M * FG) . k))) by A129, A130, A135, A171

        .= ((x1 . k) + (y1 . k)) by A126, A127, A135, A171

        .= ((x1 + y1) . k) by A169, A171, MESFUNC1:def 3;

      end;

      

       A187: ( dom (f + g)) = (( dom g) /\ ( dom g)) by A5, A7, MESFUNC2: 2

      .= ( dom g);

      now

        let x be Element of X;

        assume

         A188: x in ( dom (f + g));

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

        then

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

        g is real-valued by A4, MESFUNC2:def 4;

        then

         A190: |.(g . x).| < +infty by A187, A188, MESFUNC2:def 1;

        f is real-valued by A1, MESFUNC2:def 4;

        then |.(f . x).| < +infty by A8, A188, MESFUNC2:def 1;

        then ( |.(f . x).| + |.(g . x).|) <> +infty by A190, XXREAL_3: 16;

        hence |.((f + g) . x).| < +infty by A189, XXREAL_0: 2, XXREAL_0: 4;

      end;

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

      hence

       A191: (f + g) is_simple_func_in S by A71, A8, A107, MESFUNC2:def 4;

      thus ( dom (f + g)) <> {} by A2, A8;

      thus for x be object st x in ( dom (f + g)) holds 0. <= ((f + g) . x)

      proof

        let x be object;

        

         A193: ( dom f) c= X by RELAT_1:def 18;

        assume

         A194: x in ( dom (f + g));

         0. <= (f . x) & 0. <= (g . x) by A3, A6, SUPINF_2: 51;

        then 0. <= ((f . x) + (g . x));

        hence thesis by A8, A194, A193, MESFUNC1:def 3;

      end;

      then

       X: (f + g) is nonnegative by SUPINF_2: 52;

      ( dom FG) = ( dom c1) by A132, FINSEQ_3: 29;

      then (FG,c1) are_Re-presentation_of (f + g) by A71, A8, A138, MESFUNC3:def 1;

      then

       A195: ( integral (M,(f + g))) = ( Sum z1) by X, A2, A135, A136, A8, A191, Th3;

      ( dom (x1 + y1)) = ( Seg ( len z1)) by A169, FINSEQ_1:def 3;

      then (x1 + y1) is FinSequence by FINSEQ_1:def 2;

      then

       A196: z1 = (x1 + y1) by A169, A170, FINSEQ_1: 13;

      ( dom FG) = ( Seg ( len b1)) by A49, FINSEQ_1:def 3

      .= ( dom b1) by FINSEQ_1:def 3;

      then (FG,b1) are_Re-presentation_of g by A5, A71, A65, MESFUNC3:def 1;

      then ( integral (M,g)) = ( Sum y1) by A2, A4, A5, A6, A126, A127, Th3;

      hence thesis by A129, A126, A131, A195, A196, Th1, Y, Z;

    end;

    theorem :: MESFUNC4:6

    for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL , c be R_eal st f is_simple_func_in S & ( dom f) <> {} & f is nonnegative & 0. <= c & c < +infty & ( dom g) = ( dom f) & (for x be set st x in ( dom g) holds (g . x) = (c * (f . x))) holds ( integral (M,g)) = (c * ( integral (M,f)))

    proof

      let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X, ExtREAL , c be R_eal such that

       A1: f is_simple_func_in S and

       A2: ( dom f) <> {} and

       A3: f is nonnegative and

       A4: 0. <= c and

       A5: c < +infty and

       A6: ( dom g) = ( dom f) and

       A7: for x be set st x in ( dom g) holds (g . x) = (c * (f . x));

      for x be object st x in ( dom g) holds 0. <= (g . x)

      proof

        let x be object;

        assume

         A9: x in ( dom g);

         0. <= (f . x) by A3, SUPINF_2: 51;

        then 0. <= (c * (f . x)) by A4;

        hence thesis by A7, A9;

      end;

      then

       X: g is nonnegative by SUPINF_2: 52;

      

       A10: ex G be Finite_Sep_Sequence of S st (( dom g) = ( union ( rng G)) & for n be Nat, x,y be Element of X st n in ( dom G) & x in (G . n) & y in (G . n) holds (g . x) = (g . y))

      proof

        consider G be Finite_Sep_Sequence of S such that

         A11: ( dom f) = ( union ( rng G)) and

         A12: for n be Nat, x,y be Element of X st n in ( dom G) & x in (G . n) & y in (G . n) holds (f . x) = (f . y) by A1, MESFUNC2:def 4;

        take G;

        for n be Nat, x,y be Element of X st n in ( dom G) & x in (G . n) & y in (G . n) holds (g . x) = (g . y)

        proof

          let n be Nat;

          let x,y be Element of X;

          assume that

           A13: n in ( dom G) and

           A14: x in (G . n) and

           A15: y in (G . n);

          

           A16: (G . n) in ( rng G) by A13, FUNCT_1: 3;

          then y in ( dom g) by A6, A11, A15, TARSKI:def 4;

          then

           A17: (g . y) = (c * (f . y)) by A7;

          x in ( dom g) by A6, A11, A14, A16, TARSKI:def 4;

          then (g . x) = (c * (f . x)) by A7;

          hence thesis by A12, A13, A14, A15, A17;

        end;

        hence thesis by A6, A11;

      end;

      consider F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL , x be FinSequence of ExtREAL such that

       A18: (F,a) are_Re-presentation_of f and

       A19: ( dom x) = ( dom F) and

       A20: for n be Nat st n in ( dom x) holds (x . n) = ((a . n) * ((M * F) . n)) and

       A21: ( integral (M,f)) = ( Sum x) by A1, A2, A3, Th4;

      ex b be FinSequence of ExtREAL st ( dom b) = ( dom a) & for n be Nat st n in ( dom b) holds (b . n) = (c * (a . n))

      proof

        deffunc ca( Nat) = (c * (a . $1));

        consider b be FinSequence such that

         A22: ( len b) = ( len a) & for n be Nat st n in ( dom b) holds (b . n) = ca(n) from FINSEQ_1:sch 2;

        

         A23: ( rng b) c= ExtREAL

        proof

          let v be object;

          assume v in ( rng b);

          then

          consider k be object such that

           A24: k in ( dom b) and

           A25: v = (b . k) by FUNCT_1:def 3;

          reconsider k as Element of NAT by A24;

          v = (c * (a . k)) by A22, A24, A25;

          hence thesis;

        end;

        

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

        reconsider b as FinSequence of ExtREAL by A23, FINSEQ_1:def 4;

        take b;

        thus thesis by A22, A26, FINSEQ_1:def 3;

      end;

      then

      consider b be FinSequence of ExtREAL such that

       A27: ( dom b) = ( dom a) and

       A28: for n be Nat st n in ( dom b) holds (b . n) = (c * (a . n));

      

       A29: c in REAL by A4, A5, XXREAL_0: 14;

      ex z be FinSequence of ExtREAL st ( dom z) = ( dom x) & for n be Nat st n in ( dom z) holds (z . n) = (c * (x . n))

      proof

        deffunc cx( Nat) = (c * (x . $1));

        consider z be FinSequence such that

         A30: ( len z) = ( len x) & for n be Nat st n in ( dom z) holds (z . n) = cx(n) from FINSEQ_1:sch 2;

        

         A31: ( rng z) c= ExtREAL

        proof

          let v be object;

          assume v in ( rng z);

          then

          consider k be object such that

           A32: k in ( dom z) and

           A33: v = (z . k) by FUNCT_1:def 3;

          reconsider k as Element of NAT by A32;

          v = (c * (x . k)) by A30, A32, A33;

          hence thesis;

        end;

        

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

        reconsider z as FinSequence of ExtREAL by A31, FINSEQ_1:def 4;

        take z;

        thus thesis by A30, A34, FINSEQ_1:def 3;

      end;

      then

      consider z be FinSequence of ExtREAL such that

       A35: ( dom z) = ( dom x) and

       A36: for n be Nat st n in ( dom z) holds (z . n) = (c * (x . n));

      

       A37: for n be Nat st n in ( dom z) holds (z . n) = ((b . n) * ((M * F) . n))

      proof

        let n be Nat;

        

         A38: ( dom a) = ( dom F) by A18, MESFUNC3:def 1;

        assume

         A39: n in ( dom z);

        

        hence (z . n) = (c * (x . n)) by A36

        .= (c * ((a . n) * ((M * F) . n))) by A20, A35, A39

        .= ((c * (a . n)) * ((M * F) . n)) by XXREAL_3: 66

        .= ((b . n) * ((M * F) . n)) by A19, A27, A28, A35, A39, A38;

      end;

      

       A40: ( dom g) = ( union ( rng F)) by A6, A18, MESFUNC3:def 1;

       A41:

      now

        let n be Nat;

        assume

         A42: n in ( dom F);

        then

         A43: n in ( dom b) by A18, A27, MESFUNC3:def 1;

        let x be object;

        assume

         A44: x in (F . n);

        (F . n) in ( rng F) by A42, FUNCT_1: 3;

        then x in ( dom g) by A40, A44, TARSKI:def 4;

        

        hence (g . x) = (c * (f . x)) by A7

        .= (c * (a . n)) by A18, A42, A44, MESFUNC3:def 1

        .= (b . n) by A28, A43;

      end;

      ( dom F) = ( dom b) by A18, A27, MESFUNC3:def 1;

      then

       A45: (F,b) are_Re-presentation_of g by A40, A41, MESFUNC3:def 1;

      

       A46: f is real-valued by A1, MESFUNC2:def 4;

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

      proof

        let x be Element of X;

        assume

         A47: x in ( dom g);

        (c * (f . x)) <> -infty by A29, A46;

        then (g . x) <> -infty by A7, A47;

        then -infty < (g . x) by XXREAL_0: 6;

        then

         A48: ( - +infty ) < (g . x) by XXREAL_3:def 3;

        (c * (f . x)) <> +infty by A29, A46;

        then (g . x) <> +infty by A7, A47;

        then (g . x) < +infty by XXREAL_0: 4;

        hence thesis by A48, EXTREAL1: 22;

      end;

      then g is real-valued by MESFUNC2:def 1;

      then g is_simple_func_in S by A10, MESFUNC2:def 4;

      

      hence ( integral (M,g)) = ( Sum z) by A2, A6, A19, A35, A45, A37, Th3, X

      .= (c * ( integral (M,f))) by A29, A21, A35, A36, MESFUNC3: 10;

    end;