mesfunc3.miz



    begin

    theorem :: MESFUNC3:1

    

     Th1: for n,m be Nat, a be Function of [:( Seg n), ( Seg m):], REAL holds for p,q be FinSequence of REAL st (( dom p) = ( Seg n) & for i be Nat st i in ( dom p) holds ex r be FinSequence of REAL st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . [i, j]))) & (( dom q) = ( Seg m) & for j be Nat st j in ( dom q) holds ex s be FinSequence of REAL st (( dom s) = ( Seg n) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . [i, j]))) holds ( Sum p) = ( Sum q)

    proof

      defpred P[ Nat] means for m be Nat, a be Function of [:( Seg $1), ( Seg m):], REAL holds for p,q be FinSequence of REAL st (( dom p) = ( Seg $1) & for i be Nat st i in ( dom p) holds ex r be FinSequence of REAL st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . [i, j]))) & (( dom q) = ( Seg m) & for j be Nat st j in ( dom q) holds ex s be FinSequence of REAL st (( dom s) = ( Seg $1) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . [i, j]))) holds ( Sum p) = ( Sum q);

      

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

      proof

        let n be Nat such that

         A2: P[n];

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

        now

          let m be Nat, a be Function of [:( Seg (n + 1)), ( Seg m):], REAL ;

          let p,q be FinSequence of REAL such that

           A3: ( dom p) = ( Seg (n + 1)) and

           A4: for i be Nat st i in ( dom p) holds ex r be FinSequence of REAL st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . [i, j])) and

           A5: ( dom q) = ( Seg m) and

           A6: for j be Nat st j in ( dom q) holds ex s be FinSequence of REAL st (( dom s) = ( Seg (n + 1)) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . [i, j]));

          set a0 = (a | [:( Seg n), ( Seg m):]);

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

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

          then [:( Seg n), ( Seg m):] c= [:( Seg (n + 1)), ( Seg m):] by ZFMISC_1: 95;

          then

          reconsider a0 as Function of [:( Seg n), ( Seg m):], REAL by FUNCT_2: 32;

          deffunc F( Nat) = (a . [(n + 1), $1]);

          reconsider p0 = (p | ( Seg n)) as FinSequence of REAL by FINSEQ_1: 18;

          (n + 1) in NAT by ORDINAL1:def 12;

          then ( len p) = (n + 1) by A3, FINSEQ_1:def 3;

          then

           A7: n <= ( len p) by NAT_1: 11;

          then

           A8: ( dom p0) = ( Seg n) by FINSEQ_1: 17;

          

           A9: ( dom p0) = ( Seg n) by A7, FINSEQ_1: 17;

           A10:

          now

            let i be Nat such that

             A11: i in ( dom p0);

            consider r be FinSequence of REAL such that

             A12: ( dom r) = ( Seg m) and

             A13: (p . i) = ( Sum r) and

             A14: for j be Nat st j in ( dom r) holds (r . j) = (a . [i, j]) by A3, A4, A9, A11, FINSEQ_2: 8;

            take r;

            thus ( dom r) = ( Seg m) by A12;

            thus (p0 . i) = ( Sum r) by A11, A13, FUNCT_1: 47;

            thus for j be Nat st j in ( dom r) holds (r . j) = (a0 . [i, j])

            proof

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

              then

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

              ( dom a) = [:( Seg (n + 1)), ( Seg m):] by FUNCT_2:def 1;

              

              then

               A16: ( dom a0) = ( [:( Seg (n + 1)), ( Seg m):] /\ [:( Seg n), ( Seg m):]) by RELAT_1: 61

              .= [:( Seg n), ( Seg m):] by A15, ZFMISC_1: 101;

              let j be Nat such that

               A17: j in ( dom r);

              

               A18: [i, j] in [:( Seg n), ( Seg m):] by A9, A11, A12, A17, ZFMISC_1: 87;

              

              thus (r . j) = (a . [i, j]) by A14, A17

              .= (a0 . [i, j]) by A18, A16, FUNCT_1: 47;

            end;

          end;

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

          consider an be FinSequence such that

           A19: ( len an) = m & for j be Nat st j in ( dom an) holds (an . j) = F(j) from FINSEQ_1:sch 2;

           A20:

          now

            let i be Nat;

            assume i in ( dom an);

            then (an . i) = (a . [(n + 1), i]) by A19;

            hence (an . i) in REAL by XREAL_0:def 1;

          end;

          

           A21: ( dom an) = ( Seg m) by A19, FINSEQ_1:def 3;

          reconsider an as FinSequence of REAL by A20, FINSEQ_2: 12;

          

           A22: an is Element of (m -tuples_on REAL ) by A19, FINSEQ_2: 92;

          

           A23: ( dom an) = ( Seg m) by A19, FINSEQ_1:def 3;

          

           A24: ( Sum an) = (p . (n + 1))

          proof

            consider r be FinSequence of REAL such that

             A25: ( dom r) = ( Seg m) and

             A26: (p . (n + 1)) = ( Sum r) and

             A27: for j be Nat st j in ( dom r) holds (r . j) = (a . [(n + 1), j]) by A3, A4, FINSEQ_1: 4;

            now

              let j be Nat;

              assume

               A28: j in ( dom r);

              

              hence (r . j) = (a . [(n + 1), j]) by A27

              .= (an . j) by A19, A21, A25, A28;

            end;

            hence thesis by A23, A25, A26, FINSEQ_1: 13;

          end;

          reconsider q0 = (q - an) as FinSequence of REAL ;

          

           A29: ( rng <:q, an:>) c= [:( rng q), ( rng an):] by FUNCT_3: 51;

          ( dom diffreal ) = [: REAL , REAL :] by FUNCT_2:def 1;

          then

           A30: [:( rng q), ( rng an):] c= ( dom diffreal ) by ZFMISC_1: 96;

          ( dom ( diffreal .: (q,an))) = ( dom ( diffreal * <:q, an:>)) by FUNCOP_1:def 3

          .= ( dom <:q, an:>) by A30, A29, RELAT_1: 27, XBOOLE_1: 1

          .= (( dom q) /\ ( dom an)) by FUNCT_3:def 7;

          

          then

           A31: ( dom q0) = (( dom q) /\ ( dom an)) by RVSUM_1:def 6

          .= (( Seg m) /\ ( Seg m)) by A5, A19, FINSEQ_1:def 3

          .= ( Seg m);

          then ( len q0) = m by FINSEQ_1:def 3;

          then

           A32: q0 is Element of (m -tuples_on REAL ) by FINSEQ_2: 92;

           A33:

          now

            let j be Nat such that

             A34: j in ( dom q0);

            consider s be FinSequence of REAL such that

             A35: ( dom s) = ( Seg (n + 1)) and

             A36: (q . j) = ( Sum s) and

             A37: for i be Nat st i in ( dom s) holds (s . i) = (a . [i, j]) by A5, A6, A31, A34;

            (s . (n + 1)) = (a . [(n + 1), j]) by A35, A37, FINSEQ_1: 4;

            then

             A38: (s . (n + 1)) = (an . j) by A19, A21, A31, A34;

            reconsider sn = (s | ( Seg n)) as FinSequence of REAL by FINSEQ_1: 18;

            take sn;

            (n + 1) in NAT by ORDINAL1:def 12;

            then

             A39: ( len s) = (n + 1) by A35, FINSEQ_1:def 3;

            then n <= ( len s) by NAT_1: 11;

            hence

             A40: ( dom sn) = ( Seg n) by FINSEQ_1: 17;

            (sn ^ <*(s . (n + 1))*>) = s by A39, FINSEQ_3: 55;

            

            then ((q . j) - (an . j)) = ((( Sum sn) + (an . j)) - (an . j)) by A36, A38, RVSUM_1: 74

            .= ( Sum sn);

            hence (q0 . j) = ( Sum sn) by A34, VALUED_1: 13;

            thus for i be Nat st i in ( dom sn) holds (sn . i) = (a0 . [i, j])

            proof

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

              then

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

              ( dom a) = [:( Seg (n + 1)), ( Seg m):] by FUNCT_2:def 1;

              

              then

               A42: ( dom a0) = ( [:( Seg (n + 1)), ( Seg m):] /\ [:( Seg n), ( Seg m):]) by RELAT_1: 61

              .= [:( Seg n), ( Seg m):] by A41, ZFMISC_1: 101;

              let i be Nat such that

               A43: i in ( dom sn);

              

               A44: [i, j] in [:( Seg n), ( Seg m):] by A31, A34, A40, A43, ZFMISC_1: 87;

              

              thus (sn . i) = (s . i) by A43, FUNCT_1: 47

              .= (a . [i, j]) by A35, A37, A40, A43, A41

              .= (a0 . [i, j]) by A44, A42, FUNCT_1: 47;

            end;

          end;

          ( len q) = m by A5, FINSEQ_1:def 3;

          then q is Element of (m -tuples_on REAL ) by FINSEQ_2: 92;

          then

           A45: (q0 + an) = q by A22, RVSUM_1: 43;

          (n + 1) in NAT by ORDINAL1:def 12;

          then ( len p) = (n + 1) by A3, FINSEQ_1:def 3;

          then (p0 ^ <*( Sum an)*>) = p by A24, FINSEQ_3: 55;

          

          hence ( Sum p) = (( Sum p0) + ( Sum an)) by RVSUM_1: 74

          .= (( Sum q0) + ( Sum an)) by A2, A10, A8, A31, A33

          .= ( Sum q) by A32, A22, A45, RVSUM_1: 89;

        end;

        hence thesis;

      end;

      now

        let m be Nat, a be Function of [:( Seg 0 ), ( Seg m):], REAL ;

        let p,q be FinSequence of REAL such that

         A46: ( dom p) = ( Seg 0 ) and for i be Nat st i in ( dom p) holds ex r be FinSequence of REAL st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . [i, j])) and

         A47: ( dom q) = ( Seg m) and

         A48: for j be Nat st j in ( dom q) holds ex s be FinSequence of REAL st (( dom s) = ( Seg 0 ) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . [i, j]));

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

        now

          let z be object;

          assume

           A49: z in ( dom q);

          then z in { k where k be Nat : 1 <= k & k <= m } by A47, FINSEQ_1:def 1;

          then ex k be Nat st z = k & 1 <= k & k <= m;

          then

          reconsider j = z as Nat;

          consider s be FinSequence of REAL such that

           A50: ( dom s) = ( Seg 0 ) and

           A51: (q . j) = ( Sum s) and for i be Nat st i in ( dom s) holds (s . i) = (a . [i, j]) by A48, A49;

          s = ( <*> REAL ) by A50;

          hence (q . z) = 0 by A51, RVSUM_1: 72;

        end;

        then q = (( dom q) --> 0 ) by FUNCOP_1: 11;

        then

         A52: q = (m |-> 0 ) by A47, FINSEQ_2:def 2;

        p = ( <*> REAL ) by A46;

        hence ( Sum p) = ( Sum q) by A52, RVSUM_1: 72, RVSUM_1: 81;

      end;

      then

       A53: P[ 0 ];

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

    end;

    theorem :: MESFUNC3:2

    

     Th2: for F be FinSequence of ExtREAL , f be FinSequence of REAL st F = f holds ( Sum F) = ( Sum f)

    proof

      let F be FinSequence of ExtREAL ;

      let f be FinSequence of REAL ;

      defpred P[ Nat] means for G be FinSequence of ExtREAL , g be FinSequence of REAL st G = (F | ( Seg $1)) & g = (f | ( Seg $1)) & $1 <= ( len F) holds ( Sum G) = ( Sum g);

      (F | ( Seg ( len F))) = (F | ( len F)) by FINSEQ_1:def 15;

      then

       A1: (F | ( Seg ( len F))) = F by FINSEQ_1: 58;

      assume

       A2: F = f;

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        for G be FinSequence of ExtREAL , g be FinSequence of REAL st G = (F | ( Seg (k + 1))) & g = (f | ( Seg (k + 1))) & (k + 1) <= ( len F) holds ( Sum G) = ( Sum g)

        proof

          let G be FinSequence of ExtREAL , g be FinSequence of REAL ;

          assume that

           A5: G = (F | ( Seg (k + 1))) and

           A6: g = (f | ( Seg (k + 1))) and

           A7: (k + 1) <= ( len F);

          reconsider gk = (g . (k + 1)) as Element of REAL by XREAL_0:def 1;

          reconsider g2 = <*gk*> as FinSequence of REAL ;

          reconsider G1 = (G | ( Seg k)) as FinSequence of ExtREAL by FINSEQ_1: 18;

           A8:

          now

            

             A9: ( rng g2) c= REAL ;

            assume -infty in ( rng G1) or -infty in ( rng <*(G . (k + 1))*>);

            hence contradiction by A2, A5, A6, A9;

          end;

          reconsider g1 = (g | ( Seg k)) as FinSequence of REAL by FINSEQ_1: 18;

          ( len g) = (k + 1) by A2, A6, A7, FINSEQ_1: 17;

          then g = (g1 ^ <*(g . (k + 1))*>) by FINSEQ_3: 55;

          then

           A10: ( Sum g) = (( Sum g1) + (g . (k + 1))) by RVSUM_1: 74;

          

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

          ( len G) = (k + 1) by A5, A7, FINSEQ_1: 17;

          then G = (G1 ^ <*(G . (k + 1))*>) by FINSEQ_3: 55;

          

          then

           A12: ( Sum G) = (( Sum G1) + ( Sum <*(G . (k + 1))*>)) by A8, EXTREAL1: 10

          .= (( Sum G1) + (G . (k + 1))) by EXTREAL1: 8;

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

          then ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

          then G1 = (F | ( Seg k)) & g1 = (f | ( Seg k)) by A5, A6, FUNCT_1: 51;

          then ( Sum G1) = ( Sum g1) by A4, A7, A11, XXREAL_0: 2;

          hence thesis by A2, A5, A6, A12, A10, SUPINF_2: 1;

        end;

        hence thesis;

      end;

      

       A13: P[ 0 ] by EXTREAL1: 7, RVSUM_1: 72;

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

      hence thesis by A2, A1;

    end;

    theorem :: MESFUNC3:3

    

     Th3: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st f is_simple_func_in S holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & (for n be Nat st n in ( dom F) holds for x be object st x in (F . n) holds (f . x) = (a . n)) & for x be object st x in ( dom f) holds ex ax be FinSequence of ExtREAL st ( dom ax) = ( dom a) & for n be Nat st n in ( dom ax) holds (ax . n) = ((a . n) * (( chi ((F . n),X)) . x))

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      assume f is_simple_func_in S;

      then

      consider F be Finite_Sep_Sequence of S such that

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

       A2: for n be Nat, x,y be Element of X st n in ( dom F) & x in (F . n) & y in (F . n) holds (f . x) = (f . y) by MESFUNC2:def 4;

      defpred P[ Nat, Element of ExtREAL ] means for x be set st x in (F . $1) holds $2 = (f . x);

      

       A3: for k be Nat st k in ( Seg ( len F)) holds ex y be Element of ExtREAL st P[k, y]

      proof

        let k be Nat;

        assume k in ( Seg ( len F));

        then

         A4: k in ( dom F) by FINSEQ_1:def 3;

        then

         A5: (F . k) in ( rng F) by FUNCT_1: 3;

        per cases ;

          suppose

           A6: (F . k) = {} ;

          take y = 0. ;

          for x be set st x in (F . k) holds y = (f . x) by A6;

          hence thesis;

        end;

          suppose (F . k) <> {} ;

          then

          consider x1 be object such that

           A7: x1 in (F . k) by XBOOLE_0:def 1;

          reconsider x1 as set by TARSKI: 1;

          take y = (f . x1);

          for x be set st x in (F . k) holds y = (f . x)

          proof

            let x be set;

            

             A8: ( rng F) c= ( bool X) by XBOOLE_1: 1;

            then

            reconsider x1 as Element of X by A5, A7;

            assume

             A9: x in (F . k);

            then

            reconsider x as Element of X by A5, A8;

            (f . x) = (f . x1) by A2, A4, A7, A9;

            hence thesis;

          end;

          hence thesis;

        end;

      end;

      consider a be FinSequence of ExtREAL such that

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

      take F, a;

      

       A11: for x be set st x in ( dom f) holds ex ax be FinSequence of ExtREAL st ( dom ax) = ( dom a) & for n be Nat st n in ( dom ax) holds (ax . n) = ((a . n) * (( chi ((F . n),X)) . x))

      proof

        let x be set;

        assume x in ( dom f);

        deffunc Q( Nat) = ((a . $1) * (( chi ((F . $1),X)) . x));

        consider ax be FinSequence of ExtREAL such that

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

        take ax;

        thus thesis by A10, A12, FINSEQ_1:def 3;

      end;

      for n be Nat st n in ( dom F) holds for x be set st x in (F . n) holds (a . n) = (f . x)

      proof

        let n be Nat;

        assume n in ( dom F);

        then n in ( Seg ( len F)) by FINSEQ_1:def 3;

        hence thesis by A10;

      end;

      hence thesis by A1, A10, A11, FINSEQ_1:def 3;

    end;

    theorem :: MESFUNC3:4

    

     Th4: for X be set, F be FinSequence of X holds F is disjoint_valued iff for i,j be Nat st i in ( dom F) & j in ( dom F) & i <> j holds (F . i) misses (F . j)

    proof

      let X be set;

      let F be FinSequence of X;

      now

        assume

         A1: for i,j be Nat st i in ( dom F) & j in ( dom F) & i <> j holds (F . i) misses (F . j);

        for x,y be object st x <> y holds (F . x) misses (F . y)

        proof

          let x,y be object;

          assume

           A2: x <> y;

          per cases ;

            suppose x in ( dom F) & y in ( dom F);

            hence thesis by A1, A2;

          end;

            suppose not x in ( dom F);

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

            hence thesis;

          end;

            suppose not y in ( dom F);

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

            hence thesis;

          end;

        end;

        hence F is disjoint_valued by PROB_2:def 2;

      end;

      hence thesis by PROB_2:def 2;

    end;

    theorem :: MESFUNC3:5

    

     Th5: for X be non empty set, A be set, S be SigmaField of X, F be Finite_Sep_Sequence of S, G be FinSequence of S st ( dom G) = ( dom F) & for i be Nat st i in ( dom G) holds (G . i) = (A /\ (F . i)) holds G is Finite_Sep_Sequence of S

    proof

      let X be non empty set, A be set, S be SigmaField of X, F be Finite_Sep_Sequence of S, G be FinSequence of S such that

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

       A2: for i be Nat st i in ( dom G) holds (G . i) = (A /\ (F . i));

      now

        let i,j be Nat;

        assume that

         A3: i in ( dom G) and

         A4: j in ( dom G) and

         A5: i <> j;

        

         A6: (F . i) misses (F . j) by A1, A3, A4, A5, Th4;

        ((A /\ (F . i)) /\ (A /\ (F . j))) = (A /\ ((F . i) /\ (A /\ (F . j)))) by XBOOLE_1: 16

        .= (A /\ (((F . i) /\ (F . j)) /\ A)) by XBOOLE_1: 16

        .= (A /\ ( {} /\ A)) by A6

        .= {} ;

        then (A /\ (F . i)) misses (A /\ (F . j));

        then (G . i) misses (A /\ (F . j)) by A2, A3;

        hence (G . i) misses (G . j) by A2, A4;

      end;

      hence thesis by Th4;

    end;

    theorem :: MESFUNC3:6

    

     Th6: for X be non empty set, A be set, F,G be FinSequence of X st ( dom G) = ( dom F) & (for i be Nat st i in ( dom G) holds (G . i) = (A /\ (F . i))) holds ( union ( rng G)) = (A /\ ( union ( rng F)))

    proof

      let X be non empty set;

      let A be set;

      let F,G be FinSequence of X;

      assume that

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

       A2: for i be Nat st i in ( dom G) holds (G . i) = (A /\ (F . i));

      thus ( union ( rng G)) c= (A /\ ( union ( rng F)))

      proof

        let r be object;

        assume r in ( union ( rng G));

        then

        consider E be set such that

         A3: r in E and

         A4: E in ( rng G) by TARSKI:def 4;

        consider s be object such that

         A5: s in ( dom G) and

         A6: E = (G . s) by A4, FUNCT_1:def 3;

        reconsider s as Element of NAT by A5;

        

         A7: r in (A /\ (F . s)) by A2, A3, A5, A6;

        then

         A8: r in (F . s) by XBOOLE_0:def 4;

        (F . s) in ( rng F) by A1, A5, FUNCT_1: 3;

        then

         A9: r in ( union ( rng F)) by A8, TARSKI:def 4;

        r in A by A7, XBOOLE_0:def 4;

        hence thesis by A9, XBOOLE_0:def 4;

      end;

      let r be object;

      assume

       A10: r in (A /\ ( union ( rng F)));

      then

       A11: r in A by XBOOLE_0:def 4;

      r in ( union ( rng F)) by A10, XBOOLE_0:def 4;

      then

      consider E be set such that

       A12: r in E and

       A13: E in ( rng F) by TARSKI:def 4;

      consider s be object such that

       A14: s in ( dom F) and

       A15: E = (F . s) by A13, FUNCT_1:def 3;

      reconsider s as Element of NAT by A14;

      (A /\ E) = (G . s) by A1, A2, A14, A15;

      then

       A16: r in (G . s) by A11, A12, XBOOLE_0:def 4;

      (G . s) in ( rng G) by A1, A14, FUNCT_1: 3;

      hence thesis by A16, TARSKI:def 4;

    end;

    theorem :: MESFUNC3:7

    

     Th7: for X be set, F be FinSequence of X, i be Nat st i in ( dom F) holds (F . i) c= ( union ( rng F)) & ((F . i) /\ ( union ( rng F))) = (F . i)

    proof

      let X be set, F be FinSequence of X, i be Nat;

      assume

       A1: i in ( dom F);

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

      (F . i) in ( rng F) by A1, FUNCT_1: 3;

      hence thesis by XBOOLE_1: 28, ZFMISC_1: 74;

    end;

    theorem :: MESFUNC3:8

    

     Th8: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Finite_Sep_Sequence of S holds ( dom F) = ( dom (M * F))

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let F be Finite_Sep_Sequence of S;

      ( dom M) = S by FUNCT_2:def 1;

      then ( rng F) c= ( dom M);

      hence thesis by RELAT_1: 27;

    end;

    theorem :: MESFUNC3:9

    

     Th9: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, F be Finite_Sep_Sequence of S holds (M . ( union ( rng F))) = ( Sum (M * F))

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let F be Finite_Sep_Sequence of S;

      reconsider F1 = (M * F) as FinSequence of ExtREAL ;

      consider f be sequence of ExtREAL such that

       A1: ( Sum F1) = (f . ( len F1)) and

       A2: (f . 0 ) = 0. and

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

      consider G be Sep_Sequence of S such that

       A4: ( union ( rng F)) = ( union ( rng G)) and

       A5: for n be Nat st n in ( dom F) holds (F . n) = (G . n) and

       A6: for m be Nat st not m in ( dom F) holds (G . m) = {} by MESFUNC2: 30;

      defpred Q[ Nat] means $1 <= ( len F1) implies (( Ser (M * G)) . $1) = (f . $1);

      set G1 = (M * G);

      

       A7: ( dom G) = NAT by FUNCT_2:def 1;

      

       A9: for i be Nat st i < ( len F1) holds (( Ser (M * G)) . (i + 1)) = ((( Ser (M * G)) . i) + (F1 . (i + 1)))

      proof

        let i be Nat;

        assume i < ( len F1);

        then 1 <= (i + 1) & (i + 1) <= ( len F1) by NAT_1: 11, NAT_1: 13;

        then (i + 1) in ( dom F1) by FINSEQ_3: 25;

        then

         A10: (i + 1) in ( dom F) by Th8;

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

        

         A11: (i + 1) in NAT by ORDINAL1:def 12;

        (( Ser (M * G)) . (i + 1)) = ((( Ser (M * G)) . i) + ((M * G) . (i + 1))) by SUPINF_2:def 11

        .= ((( Ser (M * G)) . i) + (M . (G . (i + 1)))) by A7, FUNCT_1: 13, A11

        .= ((( Ser (M * G)) . i) + (M . (F . (i + 1)))) by A5, A10;

        hence thesis by A10, FUNCT_1: 13;

      end;

      

       A12: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        

         A13: for i be Nat st i < ( len F1) holds (f . (i + 1)) = ((f . i) + (F1 . (i + 1))) by A3;

        let k be Nat;

        assume

         A14: Q[k];

        assume (k + 1) <= ( len F1);

        then

         A15: k < ( len F1) by NAT_1: 13;

        then (( Ser (M * G)) . (k + 1)) = ((f . k) + (F1 . (k + 1))) by A9, A14;

        hence thesis by A13, A15;

      end;

      defpred P[ Nat] means $1 >= ( len F1) implies (( Ser (M * G)) . $1) = (( Ser (M * G)) . ( len F1));

      

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

      proof

        let k be Nat;

        assume

         A17: P[k];

        assume

         A18: (k + 1) >= ( len F1);

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

        now

          per cases ;

            case

             A19: k >= ( len F1);

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

            then not (k + 1) in ( Seg ( len F1)) by FINSEQ_1: 1;

            then not (k + 1) in ( dom F1) by FINSEQ_1:def 3;

            then

             A20: not (k + 1) in ( dom F) by Th8;

            (k + 1) in NAT by ORDINAL1:def 12;

            

            then

             A21: (G1 . (k + 1)) = (M . (G . (k + 1))) by A7, FUNCT_1: 13

            .= (M . {} ) by A6, A20

            .= 0. by VALUED_0:def 19;

            (( Ser (M * G)) . (k + 1)) = ((( Ser (M * G)) . ( len F1)) + (G1 . (k + 1))) by A17, A19, SUPINF_2:def 11;

            hence thesis by A21, XXREAL_3: 4;

          end;

            case k < ( len F1);

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

            hence thesis by A18, XXREAL_0: 1;

          end;

        end;

        hence thesis;

      end;

      defpred P1[ Nat] means $1 < ( len F1) implies (( Ser (M * G)) . (( len F1) - $1)) <= (( Ser (M * G)) . ( len F1));

      

       A22: (M * G) is nonnegative by MEASURE2: 1;

      

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

      proof

        let k be Nat;

        assume

         A24: P1[k];

        assume

         A25: (k + 1) < ( len F1);

        then

        consider k9 be Nat such that

         A26: ( len F1) = ((k + 1) qua Nat + k9) by NAT_1: 10;

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

        k <= (k + 1) & (( Ser (M * G)) . k9) <= (( Ser (M * G)) . (k9 + 1)) by A22, NAT_1: 11, SUPINF_2: 40;

        hence thesis by A24, A25, A26, XXREAL_0: 2;

      end;

       not 0 in ( Seg ( len F)) by FINSEQ_1: 1;

      then not 0 in ( dom F) by FINSEQ_1:def 3;

      then

       A27: (G . 0 ) = {} by A6;

      (( Ser (M * G)) . 0 ) = (G1 . 0 ) by SUPINF_2:def 11;

      

      then

       A28: (( Ser (M * G)) . 0 ) = (M . (G . 0 )) by A7, FUNCT_1: 13

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

      then

       A29: Q[ 0 ] by A2;

      

       A30: for k be Nat holds Q[k] from NAT_1:sch 2( A29, A12);

      

       A31: P1[ 0 ];

      

       A32: for i be Nat holds P1[i] from NAT_1:sch 2( A31, A23);

      

       A33: for i be Nat st i < ( len F1) holds (( Ser (M * G)) . i) <= (( Ser (M * G)) . ( len F1))

      proof

        let i be Nat;

        

         A34: ( len F1) <= (( len F1) + i) by NAT_1: 11;

        assume i < ( len F1);

        then

        consider k be Nat such that

         A35: ( len F1) = (i + k) by NAT_1: 10;

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

        k = (( len F1) - i) by A35;

        then

         A36: k <= ( len F1) by A34, XREAL_1: 20;

        (( Ser (M * G)) . (( len F1) - k)) <= (( Ser (M * G)) . ( len F1))

        proof

          now

            per cases by A36, XXREAL_0: 1;

              case k = ( len F1);

              hence thesis by A28, A22, SUPINF_2: 40;

            end;

              case k < ( len F1);

              hence thesis by A32;

            end;

          end;

          hence thesis;

        end;

        hence thesis by A35;

      end;

      

       A37: P[ 0 ];

      

       A38: for k be Nat holds P[k] from NAT_1:sch 2( A37, A16);

      for z be ExtReal st z in ( rng ( Ser (M * G))) holds z <= (( Ser (M * G)) . ( len F1))

      proof

        let z be ExtReal;

        assume z in ( rng ( Ser (M * G)));

        then

        consider n be object such that

         A39: n in ( dom ( Ser (M * G))) and

         A40: z = (( Ser (M * G)) . n) by FUNCT_1:def 3;

        reconsider n as Element of NAT by A39;

        now

          per cases ;

            case n < ( len F1);

            hence thesis by A33, A40;

          end;

            case n >= ( len F1);

            hence thesis by A38, A40;

          end;

        end;

        hence thesis;

      end;

      then

       A41: (( Ser (M * G)) . ( len F1)) is UpperBound of ( rng ( Ser (M * G))) by XXREAL_2:def 1;

      ( dom ( Ser (M * G))) = NAT by FUNCT_2:def 1;

      then

       A42: (( Ser (M * G)) . ( len F1)) = ( sup ( rng ( Ser (M * G)))) by A41, FUNCT_1: 3, XXREAL_2: 55;

      (M . ( union ( rng F))) = ( SUM (M * G)) by A4, MEASURE1:def 6

      .= ( sup ( rng ( Ser (M * G))));

      hence thesis by A1, A30, A42;

    end;

    theorem :: MESFUNC3:10

    

     Th10: for F,G be FinSequence of ExtREAL , a be R_eal st (a is real or (for i be Nat st i in ( dom F) holds (F . i) < 0. ) or for i be Nat st i in ( dom F) holds 0. < (F . i)) & ( dom F) = ( dom G) & for i be Nat st i in ( dom G) holds (G . i) = (a * (F . i)) holds ( Sum G) = (a * ( Sum F))

    proof

      let F,G be FinSequence of ExtREAL ;

      let a be R_eal;

      assume that

       A1: a is real or (for i be Nat st i in ( dom F) holds (F . i) < 0. ) or for i be Nat st i in ( dom F) holds 0. < (F . i) and

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

       A3: for i be Nat st i in ( dom G) holds (G . i) = (a * (F . i));

      consider g be sequence of ExtREAL such that

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

       A5: (g . 0 ) = 0. and

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

      consider f be sequence of ExtREAL such that

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

       A8: (f . 0 ) = 0. and

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

      defpred P[ Nat] means $1 <= ( len G) implies (g . $1) = (a * (f . $1));

      

       A10: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A11: P[i];

        assume

         A12: (i + 1) <= ( len G);

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

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

        then

         A13: (i + 1) in ( dom G) by A12, FINSEQ_3: 25;

        then (i + 1) in ( Seg ( len F)) by A2, FINSEQ_1:def 3;

        then (i + 1) <= ( len F) by FINSEQ_1: 1;

        then

         A14: i < ( len F) by NAT_1: 13;

        i < ( len G) by A12, NAT_1: 13;

        

        then

         A15: (g . (i + 1)) = ((g . i) + (G . (i + 1))) by A6

        .= ((a * (f . i)) + (a * (F . (i + 1)))) by A3, A11, A12, A13, NAT_1: 13;

        now

          per cases by A1;

            case a is real;

            then (g . (i + 1)) = (a * ((f . i) + (F . (i + 1)))) by A15, XXREAL_3: 95;

            hence thesis by A9, A14;

          end;

            case

             A16: for i be Nat st i in ( dom F) holds (F . i) < 0. ;

            defpred P1[ Nat] means $1 < ( len F) implies (f . $1) <= 0. ;

            

             A17: for i be Nat st P1[i] holds P1[(i + 1)]

            proof

              let i be Nat;

              assume

               A18: P1[i];

              assume

               A19: (i + 1) < ( len F);

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

              1 <= (i + 1) by NAT_1: 12;

              then (i + 1) in ( dom F) by A19, FINSEQ_3: 25;

              then

               A20: (F . (i + 1)) < 0. by A16;

              i < ( len F) by A19, NAT_1: 13;

              then (f . (i + 1)) = ((f . i) + (F . (i + 1))) by A9;

              hence thesis by A18, A19, A20, NAT_1: 13;

            end;

            

             A21: P1[ 0 ] by A8;

            for i be Nat holds P1[i] from NAT_1:sch 2( A21, A17);

            then

             A22: (f . i) < 0. or (f . i) = 0. by A14;

            (F . (i + 1)) < 0. by A2, A13, A16;

            then (g . (i + 1)) = (a * ((f . i) + (F . (i + 1)))) by A15, A22, XXREAL_3: 97;

            hence thesis by A9, A14;

          end;

            case

             A23: for i be Nat st i in ( dom F) holds 0. < (F . i);

            defpred P2[ Nat] means $1 < ( len F) implies 0. <= (f . $1);

            

             A24: for i be Nat st P2[i] holds P2[(i + 1)]

            proof

              let i be Nat;

              assume

               A25: P2[i];

              assume

               A26: (i + 1) < ( len F);

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

              1 <= (i + 1) by NAT_1: 12;

              then (i + 1) in ( dom F) by A26, FINSEQ_3: 25;

              then

               A27: 0. < (F . (i + 1)) by A23;

              i < ( len F) by A26, NAT_1: 13;

              then (f . (i + 1)) = ((f . i) + (F . (i + 1))) by A9;

              hence thesis by A25, A26, A27, NAT_1: 13;

            end;

            

             A28: P2[ 0 ] by A8;

            for i be Nat holds P2[i] from NAT_1:sch 2( A28, A24);

            then

             A29: 0. < (f . i) or (f . i) = 0. by A14;

             0. < (F . (i + 1)) by A2, A13, A23;

            then (g . (i + 1)) = (a * ((f . i) + (F . (i + 1)))) by A15, A29, XXREAL_3: 96;

            hence thesis by A9, A14;

          end;

        end;

        hence thesis;

      end;

      

       A30: P[ 0 ] by A8, A5;

      

       A31: for i be Nat holds P[i] from NAT_1:sch 2( A30, A10);

      ( Seg ( len F)) = ( dom G) by A2, FINSEQ_1:def 3

      .= ( Seg ( len G)) by FINSEQ_1:def 3;

      

      then (a * ( Sum F)) = (a * (f . ( len G))) by A7, FINSEQ_1: 6

      .= (g . ( len G)) by A31;

      hence thesis by A4;

    end;

    theorem :: MESFUNC3:11

    

     Th11: for F be FinSequence of REAL holds F is FinSequence of ExtREAL

    proof

      let F be FinSequence of REAL ;

      ( rng F) c= ExtREAL by NUMBERS: 31;

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      let F be Finite_Sep_Sequence of S;

      let a be FinSequence of ExtREAL ;

      :: MESFUNC3:def1

      pred F,a are_Re-presentation_of f means ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & for n be Nat st n in ( dom F) holds for x be object st x in (F . n) holds (f . x) = (a . n);

    end

    theorem :: MESFUNC3:12

    for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st f is_simple_func_in S holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st (F,a) are_Re-presentation_of f

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      assume f is_simple_func_in S;

      then

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

       A1: ( dom f) = ( union ( rng F)) & ( dom F) = ( dom a) & for n be Nat st n in ( dom F) holds for x be object st x in (F . n) holds (f . x) = (a . n) and for x be object st x in ( dom f) holds ex ax be FinSequence of ExtREAL st ( dom ax) = ( dom a) & for n be Nat st n in ( dom ax) holds (ax . n) = ((a . n) * (( chi ((F . n),X)) . x)) by Th3;

      take F, a;

      thus thesis by A1;

    end;

    theorem :: MESFUNC3:13

    

     Th13: for X be non empty set, S be SigmaField of X, F be Finite_Sep_Sequence of S holds ex G be Finite_Sep_Sequence of S st ( union ( rng F)) = ( union ( rng G)) & for n be Nat st n in ( dom G) holds ((G . n) <> {} & ex m be Nat st m in ( dom F) & (F . m) = (G . n))

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let F be Finite_Sep_Sequence of S;

      defpred P[ Nat] means for F be Finite_Sep_Sequence of S st ( len F) = $1 holds ex G be Finite_Sep_Sequence of S st (( union ( rng F)) = ( union ( rng G)) & (for n be Nat st n in ( dom G) holds ((G . n) <> {} & ex m be Nat st m in ( dom F) & (F . m) = (G . n))));

      

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

      proof

        let n be Nat;

        assume

         A2: P[n];

        let F be Finite_Sep_Sequence of S;

        assume

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

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

        reconsider F1 = (F | ( Seg n)) as Finite_Sep_Sequence of S by MESFUNC2: 33;

        

         A4: n <= ( len F) by A3, NAT_1: 11;

        then

         A5: ( len F1) = n by FINSEQ_1: 17;

        then

        consider G1 be Finite_Sep_Sequence of S such that

         A6: ( union ( rng F1)) = ( union ( rng G1)) and

         A7: for n be Nat st n in ( dom G1) holds ((G1 . n) <> {} & ex m be Nat st m in ( dom F1) & (F1 . m) = (G1 . n)) by A2;

        

         A8: ( dom F) = ( dom (F1 ^ <*(F . (n + 1))*>)) & for k be Nat st k in ( dom F) holds (F . k) = ((F1 ^ <*(F . (n + 1))*>) . k)

        proof

          

          thus ( dom (F1 ^ <*(F . (n + 1))*>)) = ( Seg (( len F1) + ( len <*(F . (n + 1))*>))) by FINSEQ_1:def 7

          .= ( Seg (n + 1)) by A5, FINSEQ_1: 39

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

          let k be Nat;

          assume

           A9: k in ( dom F);

          now

            per cases ;

              case

               A10: k in ( dom F1);

              then k in ( Seg n) by A4, FINSEQ_1: 17;

              then k <= n by FINSEQ_1: 1;

              then

               A11: ((F | n) . k) = (F . k) by FINSEQ_3: 112;

              ((F1 ^ <*(F . (n + 1))*>) . k) = (F1 . k) by A10, FINSEQ_1:def 7;

              hence thesis by A11, FINSEQ_1:def 15;

            end;

              case

               A12: not k in ( dom F1);

              

               A13: k in ( Seg (n + 1)) by A3, A9, FINSEQ_1:def 3;

               not k in ( Seg n) by A4, A12, FINSEQ_1: 17;

              then not (1 <= k & k <= n) by FINSEQ_1: 1;

              then

               A14: not k < (n + 1) by A13, FINSEQ_1: 1, NAT_1: 13;

              ( dom <*(F . (n + 1))*>) = ( Seg 1) by FINSEQ_1:def 8;

              then

               A15: 1 in ( dom <*(F . (n + 1))*>) by FINSEQ_1: 2, TARSKI:def 1;

              

               A16: k <= (n + 1) by A13, FINSEQ_1: 1;

              

              then ((F1 ^ <*(F . (n + 1))*>) . k) = ((F1 ^ <*(F . (n + 1))*>) . (( len F1) + 1)) by A5, A14, XXREAL_0: 1

              .= ( <*(F . (n + 1))*> . 1) by A15, FINSEQ_1:def 7

              .= (F . (n + 1)) by FINSEQ_1:def 8;

              hence thesis by A14, A16, XXREAL_0: 1;

            end;

          end;

          hence thesis;

        end;

        then

         A17: F = (F1 ^ <*(F . (n + 1))*>) by FINSEQ_1: 13;

        ex G be Finite_Sep_Sequence of S st ( union ( rng F)) = ( union ( rng G)) & for k be Nat st k in ( dom G) holds ((G . k) <> {} & ex m be Nat st m in ( dom F) & (F . m) = (G . k))

        proof

          now

            per cases ;

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

              then

               A18: ( rng <*(F . (n + 1))*>) = { {} } by FINSEQ_1: 38;

              take G = G1;

              

               A19: for k be Nat st k in ( dom G) holds ((G . k) <> {} & ex m be Nat st m in ( dom F) & (F . m) = (G . k))

              proof

                let k be Nat;

                

                 A20: ( dom F1) c= ( dom F) by A8, FINSEQ_1: 26;

                assume

                 A21: k in ( dom G);

                then

                consider m be Nat such that

                 A22: m in ( dom F1) and

                 A23: (F1 . m) = (G . k) by A7;

                (F1 . m) = (F . m) by A17, A22, FINSEQ_1:def 7;

                hence thesis by A7, A21, A22, A23, A20;

              end;

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

              

              then ( union ( rng F)) = (( union ( rng F1)) \/ ( union ( rng <*(F . (n + 1))*>))) by ZFMISC_1: 78

              .= (( union ( rng F1)) \/ {} ) by A18, ZFMISC_1: 25

              .= ( union ( rng G)) by A6;

              hence thesis by A19;

            end;

              case

               A24: (F . (n + 1)) <> {} ;

              

               A25: for k,m be object st k <> m holds ((G1 ^ <*(F . (n + 1))*>) . k) misses ((G1 ^ <*(F . (n + 1))*>) . m)

              proof

                let k,m be object;

                assume

                 A26: k <> m;

                now

                  per cases ;

                    case

                     A27: k in ( dom (G1 ^ <*(F . (n + 1))*>)) & m in ( dom (G1 ^ <*(F . (n + 1))*>));

                    then

                    reconsider k, m as Element of NAT ;

                    now

                      per cases ;

                        case k = ( len (G1 ^ <*(F . (n + 1))*>));

                        then k = (( len G1) + ( len <*(F . (n + 1))*>)) by FINSEQ_1: 22;

                        then

                         A28: k = (( len G1) + 1) by FINSEQ_1: 39;

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

                        

                        then

                         A29: ((G1 ^ <*(F . (n + 1))*>) . k) = ( <*(F . (n + 1))*> . 1) by A28, FINSEQ_1: 65

                        .= (F . (n + 1)) by FINSEQ_1:def 8;

                        

                         A30: m in ( Seg ( len (G1 ^ <*(F . (n + 1))*>))) by A27, FINSEQ_1:def 3;

                        then m in ( Seg (( len G1) + ( len <*(F . (n + 1))*>))) by FINSEQ_1: 22;

                        then m in ( Seg (( len G1) + 1)) by FINSEQ_1: 39;

                        then m <= (( len G1) + 1) by FINSEQ_1: 1;

                        then m < (( len G1) + 1) by A26, A28, XXREAL_0: 1;

                        then

                         A31: m <= ( len G1) by NAT_1: 13;

                        1 <= m by A30, FINSEQ_1: 1;

                        then

                         A32: m in ( dom G1) by A31, FINSEQ_3: 25;

                        then

                        consider m1 be Nat such that

                         A33: m1 in ( dom F1) and

                         A34: (F1 . m1) = (G1 . m) by A7;

                        m1 in ( Seg ( len F1)) by A33, FINSEQ_1:def 3;

                        then m1 <= n by A5, FINSEQ_1: 1;

                        then

                         A35: m1 <> (n + 1) by NAT_1: 13;

                        ((G1 ^ <*(F . (n + 1))*>) . m) = (G1 . m) by A32, FINSEQ_1:def 7;

                        then ((G1 ^ <*(F . (n + 1))*>) . m) = (F . m1) by A17, A33, A34, FINSEQ_1:def 7;

                        hence thesis by A29, A35, PROB_2:def 2;

                      end;

                        case k <> ( len (G1 ^ <*(F . (n + 1))*>));

                        then k <> (( len G1) + ( len <*(F . (n + 1))*>)) by FINSEQ_1: 22;

                        then

                         A36: k <> (( len G1) + 1) by FINSEQ_1: 39;

                        

                         A37: k in ( Seg ( len (G1 ^ <*(F . (n + 1))*>))) by A27, FINSEQ_1:def 3;

                        then k in ( Seg (( len G1) + ( len <*(F . (n + 1))*>))) by FINSEQ_1: 22;

                        then k in ( Seg (( len G1) + 1)) by FINSEQ_1: 39;

                        then k <= (( len G1) + 1) by FINSEQ_1: 1;

                        then k < (( len G1) + 1) by A36, XXREAL_0: 1;

                        then

                         A38: k <= ( len G1) by NAT_1: 13;

                        1 <= k by A37, FINSEQ_1: 1;

                        then

                         A39: k in ( dom G1) by A38, FINSEQ_3: 25;

                        then

                         A40: ((G1 ^ <*(F . (n + 1))*>) . k) = (G1 . k) by FINSEQ_1:def 7;

                        now

                          per cases ;

                            case m = ( len (G1 ^ <*(F . (n + 1))*>));

                            then m = (( len G1) + ( len <*(F . (n + 1))*>)) by FINSEQ_1: 22;

                            then

                             A41: m = (( len G1) + 1) by FINSEQ_1: 39;

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

                            

                            then

                             A42: ((G1 ^ <*(F . (n + 1))*>) . m) = ( <*(F . (n + 1))*> . 1) by A41, FINSEQ_1: 65

                            .= (F . (n + 1)) by FINSEQ_1:def 8;

                            consider k1 be Nat such that

                             A43: k1 in ( dom F1) and

                             A44: (F1 . k1) = (G1 . k) by A7, A39;

                            k1 in ( Seg ( len F1)) by A43, FINSEQ_1:def 3;

                            then k1 <= n by A5, FINSEQ_1: 1;

                            then

                             A45: k1 <> (n + 1) by NAT_1: 13;

                            ((G1 ^ <*(F . (n + 1))*>) . k) = (F . k1) by A17, A40, A43, A44, FINSEQ_1:def 7;

                            hence thesis by A42, A45, PROB_2:def 2;

                          end;

                            case m <> ( len (G1 ^ <*(F . (n + 1))*>));

                            then m <> (( len G1) + ( len <*(F . (n + 1))*>)) by FINSEQ_1: 22;

                            then

                             A46: m <> (( len G1) + 1) by FINSEQ_1: 39;

                            

                             A47: m in ( Seg ( len (G1 ^ <*(F . (n + 1))*>))) by A27, FINSEQ_1:def 3;

                            then m in ( Seg (( len G1) + ( len <*(F . (n + 1))*>))) by FINSEQ_1: 22;

                            then m in ( Seg (( len G1) + 1)) by FINSEQ_1: 39;

                            then m <= (( len G1) + 1) by FINSEQ_1: 1;

                            then m < (( len G1) + 1) by A46, XXREAL_0: 1;

                            then

                             A48: m <= ( len G1) by NAT_1: 13;

                            1 <= m by A47, FINSEQ_1: 1;

                            then m in ( dom G1) by A48, FINSEQ_3: 25;

                            then ((G1 ^ <*(F . (n + 1))*>) . m) = (G1 . m) by FINSEQ_1:def 7;

                            hence thesis by A26, A40, PROB_2:def 2;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                    case not (k in ( dom (G1 ^ <*(F . (n + 1))*>)) & m in ( dom (G1 ^ <*(F . (n + 1))*>)));

                    then ((G1 ^ <*(F . (n + 1))*>) . k) = {} or ((G1 ^ <*(F . (n + 1))*>) . m) = {} by FUNCT_1:def 2;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              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 A3, FINSEQ_1:def 3;

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

              then <*(F . (n + 1))*> is FinSequence of S by FINSEQ_1: 74;

              then

              reconsider G = (G1 ^ <*(F . (n + 1))*>) as Finite_Sep_Sequence of S by A25, FINSEQ_1: 75, PROB_2:def 2;

              

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

              .= (( len G1) + 1) by FINSEQ_1: 39;

              

               A50: for k be Nat st k in ( dom G) holds ((G . k) <> {} & ex m be Nat st m in ( dom F) & (F . m) = (G . k))

              proof

                let k be Nat;

                assume

                 A51: k in ( dom G);

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

                now

                  per cases ;

                    case

                     A52: k = ( len G);

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

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

                    then

                     A53: (n + 1) in ( dom F) by A3, FINSEQ_1:def 3;

                    ( dom <*(F . (n + 1))*>) = ( Seg 1) by FINSEQ_1: 38;

                    then 1 in ( dom <*(F . (n + 1))*>) by FINSEQ_1: 2, TARSKI:def 1;

                    

                    then (G . k) = ( <*(F . (n + 1))*> . 1) by A49, A52, FINSEQ_1:def 7

                    .= (F . (n + 1)) by FINSEQ_1:def 8;

                    hence thesis by A24, A53;

                  end;

                    case

                     A54: k <> ( len G);

                    k <= ( len G) by A51, FINSEQ_3: 25;

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

                    then

                     A55: k <= ( len G1) by A49, NAT_1: 13;

                    1 <= k by A51, FINSEQ_3: 25;

                    then

                     A56: k in ( dom G1) by A55, FINSEQ_3: 25;

                    then

                     A57: (G . k) = (G1 . k) by FINSEQ_1:def 7;

                    ex m be Nat st m in ( dom F) & (F . m) = (G . k)

                    proof

                      consider m be Nat such that

                       A58: m in ( dom F1) & (F1 . m) = (G1 . k) by A7, A56;

                      take m;

                      ( dom F1) c= ( dom F) by A8, FINSEQ_1: 26;

                      hence thesis by A17, A57, A58, FINSEQ_1:def 7;

                    end;

                    hence thesis by A7, A56, A57;

                  end;

                end;

                hence thesis;

              end;

              take G;

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

              

              then ( union ( rng F)) = (( union ( rng F1)) \/ ( union ( rng <*(F . (n + 1))*>))) by ZFMISC_1: 78

              .= ( union (( rng G1) \/ ( rng <*(F . (n + 1))*>))) by A6, ZFMISC_1: 78

              .= ( union ( rng G)) by FINSEQ_1: 31;

              hence thesis by A50;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      

       A59: ( len F) = ( len F);

      

       A60: P[ 0 ]

      proof

        let F be Finite_Sep_Sequence of S;

        assume

         A61: ( len F) = 0 ;

        take G = F;

        G = {} by A61;

        hence thesis;

      end;

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

      hence thesis by A59;

    end;

    

     Lm1: for a be FinSequence of ExtREAL , p,N be Element of ExtREAL st N = ( len a) & (for n be Nat st n in ( dom a) holds (a . n) = p) holds ( Sum a) = (N * p)

    proof

      defpred P[ Nat] means for F be FinSequence of ExtREAL , p be Element of ExtREAL st $1 = ( len F) & (for n be Nat st n in ( dom F) holds (F . n) = p) holds ex N be Element of ExtREAL st N = $1 & ( Sum F) = (N * p);

      let a be FinSequence of ExtREAL ;

      let p,N be Element of ExtREAL ;

      assume that

       A1: N = ( len a) and

       A2: for n be Nat st n in ( dom a) holds (a . n) = p;

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

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

        for F be FinSequence of ExtREAL , p be Element of ExtREAL st (k + 1) = ( len F) & (for n be Nat st n in ( dom F) holds (F . n) = p) holds ex N be Element of ExtREAL st N = (k + 1) & ( Sum F) = (N * p)

        proof

          let F be FinSequence of ExtREAL ;

          let p be Element of ExtREAL ;

          assume that

           A5: (k + 1) = ( len F) and

           A6: for n be Nat st n in ( dom F) holds (F . n) = p;

          F <> {} by A5;

          then

          consider G be FinSequence, v be object such that

           A7: F = (G ^ <*v*>) by FINSEQ_1: 46;

          reconsider G as FinSequence of ExtREAL by A7, FINSEQ_1: 36;

          

           A8: (k + 1) = (( len G) + ( len <*v*>)) by A5, A7, FINSEQ_1: 22

          .= (( len G) + 1) by FINSEQ_1: 39;

          ( dom <*v*>) = ( Seg 1) by FINSEQ_1: 38;

          then

           A9: 1 in ( dom <*v*>) by FINSEQ_1: 2, TARSKI:def 1;

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

          then

           A10: (k + 1) in ( dom F) by A5, FINSEQ_3: 25;

          v = ( <*v*> . 1) by FINSEQ_1: 40

          .= (F . (k + 1)) by A7, A8, A9, FINSEQ_1:def 7

          .= p by A6, A10;

          then

          reconsider v as Element of ExtREAL ;

          consider g be sequence of ExtREAL such that

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

           A12: (g . 0 ) = 0. and

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

          for n be Nat st n in ( dom G) holds (G . n) = p

          proof

            let n be Nat;

            

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

            assume

             A15: n in ( dom G);

            then n <= ( len G) by FINSEQ_3: 25;

            then

             A16: n <= (( len G) + 1) by A14, XXREAL_0: 2;

            

             A17: ( len F) = (( len G) + ( len <*v*>)) by A7, FINSEQ_1: 22

            .= (( len G) + 1) by FINSEQ_1: 39;

            1 <= n by A15, FINSEQ_3: 25;

            then n in ( dom F) by A16, A17, FINSEQ_3: 25;

            then (F . n) = p by A6;

            hence thesis by A7, A15, FINSEQ_1:def 7;

          end;

          then

          consider N1 be Element of ExtREAL such that

           A18: N1 = k and

           A19: ( Sum G) = (N1 * p) by A4, A8;

          consider f be sequence of ExtREAL such that

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

           A21: (f . 0 ) = 0. and

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

          

           A23: for k1 be Nat st k1 <= ( len G) holds (f . k1) = (g . k1)

          proof

            defpred P2[ Nat] means $1 <= ( len G) implies (f . $1) = (g . $1);

            

             A24: for k1 be Nat st P2[k1] holds P2[(k1 + 1)]

            proof

              let k1 be Nat;

              assume

               A25: P2[k1];

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

              now

                assume

                 A26: (k1 + 1) <= ( len G);

                then

                 A27: k1 < ( len G) by NAT_1: 13;

                ( len F) = (( len G) + ( len <*v*>)) by A7, FINSEQ_1: 22

                .= (( len G) + 1) by FINSEQ_1: 39;

                then k1 < ( len F) by A27, NAT_1: 13;

                then

                 A28: (f . (k1 + 1)) = ((f . k1) + (F . (k1 + 1))) by A22;

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

                then

                 A29: (k1 + 1) in ( dom G) by A26, FINSEQ_3: 25;

                k1 <= (k1 + 1) & (g . (k1 + 1)) = ((g . k1) + (G . (k1 + 1))) by A13, A27, NAT_1: 11;

                hence thesis by A7, A25, A28, A29, FINSEQ_1:def 7, XXREAL_0: 2;

              end;

              hence thesis;

            end;

            

             A30: P2[ 0 ] by A21, A12;

            for k1 be Nat holds P2[k1] from NAT_1:sch 2( A30, A24);

            hence thesis;

          end;

          take (N1 + 1. );

          reconsider jj = 1 as Real;

          

          thus (N1 + 1. ) = (k + jj) by A18, SUPINF_2: 1

          .= (k + 1);

          k < ( len F) by A5, NAT_1: 13;

          

          then ( Sum F) = ((f . k) + (F . (k + 1))) by A5, A20, A22

          .= ((g . k) + (F . (k + 1))) by A8, A23;

          

          then ( Sum F) = (( Sum G) + p) by A6, A8, A10, A11

          .= ((N1 * p) + ( 1. * p)) by A19, XXREAL_3: 81;

          hence ( Sum F) = ((N1 + 1. ) * p) by A18, XXREAL_3: 96;

        end;

        hence thesis;

      end;

      for F be FinSequence of ExtREAL , p be Element of ExtREAL st 0 = ( len F) & (for n be Nat st n in ( dom F) holds (F . n) = p) holds ex N be Element of ExtREAL st N = 0 & ( Sum F) = (N * p)

      proof

        let F be FinSequence of ExtREAL ;

        let p be Element of ExtREAL ;

        assume that

         A31: 0 = ( len F) and for n be Nat st n in ( dom F) holds (F . n) = p;

        take 0. ;

        ex f be sequence of ExtREAL st ( Sum F) = (f . ( len F)) & (f . 0 ) = 0. & for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1))) by EXTREAL1:def 2;

        hence thesis by A31;

      end;

      then

       A32: P[ 0 ];

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

      then ex N9 be Element of ExtREAL st N9 = ( len a) & ( Sum a) = (N9 * p) by A2;

      hence thesis by A1;

    end;

    

     Lm2: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st f is_simple_func_in S & f is nonnegative & (for x be object st x in ( dom f) holds 0. <> (f . x)) holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st (F,a) are_Re-presentation_of f & (a . 1) = 0. & for n be Nat st 2 <= n & n in ( dom a) holds 0. < (a . n) & (a . n) < +infty

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      assume that

       A1: f is_simple_func_in S and

       A2: f is nonnegative and

       A3: for x be object st x in ( dom f) holds 0. <> (f . x);

      

       a2: for x be object st x in ( dom f) holds 0. <= (f . x) by A2, SUPINF_2: 39;

      consider F1 be Finite_Sep_Sequence of S such that

       A4: ( dom f) = ( union ( rng F1)) and

       A5: for n be Nat, x,y be Element of X st n in ( dom F1) & x in (F1 . n) & y in (F1 . n) holds (f . x) = (f . y) by A1, MESFUNC2:def 4;

      consider G be Finite_Sep_Sequence of S such that

       A6: ( union ( rng F1)) = ( union ( rng G)) and

       A7: for n be Nat st n in ( dom G) holds ((G . n) <> {} & ex m be Nat st m in ( dom F1) & (F1 . m) = (G . n)) by Th13;

      set F = ( <* {} *> ^ G);

      ( rng <* {} *>) = { {} } & {} in S by FINSEQ_1: 38, MEASURE1: 7;

      then ( rng <* {} *>) c= S by ZFMISC_1: 31;

      then (( rng <* {} *>) \/ ( rng G)) c= S by XBOOLE_1: 8;

      then ( rng F) c= S by FINSEQ_1: 31;

      then

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

      for x,y be object st x <> y holds (F . x) misses (F . y)

      proof

        let x,y be object;

        assume

         A8: x <> y;

        now

          per cases ;

            case

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

            then

            reconsider x, y as Element of NAT ;

            

             A10: x in ( Seg ( len ( <* {} *> ^ G))) by A9, FINSEQ_1:def 3;

            then

             A11: x <= ( len ( <* {} *> ^ G)) by FINSEQ_1: 1;

            

             A12: y in ( Seg ( len ( <* {} *> ^ G))) by A9, FINSEQ_1:def 3;

            then

             A13: 1 <= y by FINSEQ_1: 1;

            

             A14: y <= ( len ( <* {} *> ^ G)) by A12, FINSEQ_1: 1;

            

             A15: 1 <= x by A10, FINSEQ_1: 1;

            now

              per cases ;

                case

                 A16: x = 1 or y = 1;

                

                 A17: ( dom <* {} *>) = ( Seg 1) by FINSEQ_1: 38;

                now

                  per cases by A16;

                    case

                     A18: x = 1;

                    then x in ( dom <* {} *>) by A17, FINSEQ_1: 2, TARSKI:def 1;

                    then (F . x) = ( <* {} *> . x) by FINSEQ_1:def 7;

                    then (F . x) = {} by A18, FINSEQ_1:def 8;

                    hence thesis;

                  end;

                    case

                     A19: y = 1;

                    then y in ( dom <* {} *>) by A17, FINSEQ_1: 2, TARSKI:def 1;

                    then (F . y) = ( <* {} *> . y) by FINSEQ_1:def 7;

                    then (F . y) = {} by A19, FINSEQ_1:def 8;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

                case

                 A20: x <> 1 & y <> 1;

                then 1 < y by A13, XXREAL_0: 1;

                then ( len <* {} *>) < y by FINSEQ_1: 40;

                then

                 A21: (F . y) = (G . (y - ( len <* {} *>))) by A14, FINSEQ_1: 24;

                1 < x by A15, A20, XXREAL_0: 1;

                then ( len <* {} *>) < x by FINSEQ_1: 40;

                then

                 A22: (F . x) = (G . (x - ( len <* {} *>))) by A11, FINSEQ_1: 24;

                (x - ( len <* {} *>)) <> (y - ( len <* {} *>)) by A8;

                hence thesis by A22, A21, PROB_2:def 2;

              end;

            end;

            hence thesis;

          end;

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

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

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then

      reconsider F as Finite_Sep_Sequence of S by PROB_2:def 2;

      

       A23: ( union ( rng F)) = ( union (( rng <* {} *>) \/ ( rng G))) by FINSEQ_1: 31

      .= ( union ( { {} } \/ ( rng G))) by FINSEQ_1: 38

      .= (( union { {} }) \/ ( union ( rng G))) by ZFMISC_1: 78

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

      .= ( dom f) by A4, A6;

      defpred P[ Nat, Element of ExtREAL ] means (for x be Element of X st $1 in ( dom F) & $1 = 1 holds $2 = 0. ) & (for x be Element of X st $1 in ( dom F) & $1 >= 2 & x in (F . $1) holds $2 = (f . x));

      

       A24: for k be Nat st k in ( Seg ( len F)) holds ex y be Element of ExtREAL st P[k, y]

      proof

        let k be Nat;

        assume

         A25: k in ( Seg ( len F));

        ex y be Element of ExtREAL st P[k, y]

        proof

          per cases ;

            suppose

             A26: k = 1;

            take y = 0. ;

            (for x be Element of X st k in ( dom F) & k = 1 holds y = 0. ) & for x be Element of X st k in ( dom F) & k >= 2 & x in (F . k) holds y = (f . x) by A26;

            hence thesis;

          end;

            suppose

             A27: k <> 1;

            

             A28: k <= ( len F) by A25, FINSEQ_1: 1;

            then k <= (( len <* {} *>) + ( len G)) by FINSEQ_1: 22;

            then

             A29: (k - ( len <* {} *>)) <= ( len G) by XREAL_1: 20;

            1 <= k by A25, FINSEQ_1: 1;

            then 1 < k by A27, XXREAL_0: 1;

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

            then

             A30: (( len <* {} *>) + 1) <= k by FINSEQ_1: 39;

            then

            consider k2 be Nat such that

             A31: ((( len <* {} *>) + 1) + k2) = k by NAT_1: 10;

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

            (1 + k2) = (k - ( len <* {} *>)) by A31;

            then 1 <= (1 + k2) by A30, XREAL_1: 19;

            then (1 + k2) in ( Seg ( len G)) by A31, A29, FINSEQ_1: 1;

            then

             A32: (1 + k2) in ( dom G) by FINSEQ_1:def 3;

            then

            consider m1 be Nat such that

             A33: m1 in ( dom F1) and

             A34: (F1 . m1) = (G . (1 + k2)) by A7;

            k <= (( len <* {} *>) + ( len G)) by A28, FINSEQ_1: 22;

            

            then

             A35: (F . k) = (G . (k - ( len <* {} *>))) by A30, FINSEQ_1: 23

            .= (G . (1 + k2)) by A31;

            then (F . k) <> {} by A7, A32;

            then

            consider z be object such that

             A36: z in (F . k) by XBOOLE_0:def 1;

            reconsider z as set by TARSKI: 1;

            take y = (f . z);

            (F . k) in ( rng F1) by A35, A33, A34, FUNCT_1: 3;

            then (F . k) in S;

            then

            reconsider z as Element of X by A36;

            

             A37: for x be Element of X st k in ( dom F) & k >= 2 & x in (F . k) holds y = (f . x)

            proof

              let x be Element of X;

              assume that k in ( dom F) and k >= 2 and

               A38: x in (F . k);

              z in (F1 . m1) by A35, A36, A34;

              hence thesis by A5, A35, A33, A34, A38;

            end;

            for x be Element of X st k in ( dom F) & k = 1 holds y = 0. by A27;

            hence thesis by A37;

          end;

        end;

        hence thesis;

      end;

      consider a be FinSequence of ExtREAL such that

       A39: ( dom a) = ( Seg ( len F)) & for n be Nat st n in ( Seg ( len F)) holds P[n, (a . n)] from FINSEQ_1:sch 5( A24);

      

       A40: ( dom F) = ( dom a) by A39, FINSEQ_1:def 3;

      

       A41: for n be Nat, x be Element of X st n in ( dom F) & n >= 2 & x in (F . n) holds (a . n) = (f . x)

      proof

        let n be Nat;

        let x be Element of X;

        assume that

         A42: n in ( dom F) and

         A43: n >= 2 & x in (F . n);

        n in ( Seg ( len F)) by A42, FINSEQ_1:def 3;

        hence thesis by A39, A42, A43;

      end;

      

       A44: for n be Nat st 2 <= n & n in ( dom a) holds 0. < (a . n) & (a . n) < +infty

      proof

        let n be Nat;

        assume that

         A45: 2 <= n and

         A46: n in ( dom a);

        (1 + 1) <= n by A45;

        then

         A47: (( len <* {} *>) + 1) <= n by FINSEQ_1: 39;

        n <= ( len F) by A39, A46, FINSEQ_1: 1;

        then n <= (( len <* {} *>) + ( len G)) by FINSEQ_1: 22;

        

        then

         A48: (F . n) = (G . (n - ( len <* {} *>))) by A47, FINSEQ_1: 23

        .= (G . (n - 1)) by FINSEQ_1: 39;

        ( dom <* {} *>) = {1} & 1 <> n by A45, FINSEQ_1: 2, FINSEQ_1: 38;

        then not n in ( dom <* {} *>) by TARSKI:def 1;

        then

        consider k be Nat such that

         A49: k in ( dom G) and

         A50: n = (( len <* {} *>) + k) by A40, A46, FINSEQ_1: 25;

        n = (1 + k) by A50, FINSEQ_1: 39;

        then (F . n) <> {} by A7, A48, A49;

        then

        consider x1 be object such that

         A51: x1 in (F . n) by XBOOLE_0:def 1;

        

         A52: (F . n) c= ( union ( rng F)) by A40, A46, FUNCT_1: 3, ZFMISC_1: 74;

        then x1 in ( dom f) by A23, A51;

        then

        reconsider x1 as Element of X;

        

         A53: 0. <> (f . x1) by A3, A23, A51, A52;

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

        then

         A54: |.(f . x1).| < +infty by A23, A51, A52, MESFUNC2:def 1;

        (a . n) = (f . x1) by A41, A40, A45, A46, A51;

        hence thesis by A23, A51, A52, A54, A53, EXTREAL1: 21, a2;

      end;

      take F, a;

      

       A55: for n9 be Nat st n9 in ( dom F) holds for x be object st x in (F . n9) holds (f . x) = (a . n9)

      proof

        let n9 be Nat;

        assume

         A56: n9 in ( dom F);

        now

          per cases ;

            case

             A57: n9 = 1;

            thus for x be set st x in (F . n9) holds (f . x) = (a . n9)

            proof

              let x be set;

              ( dom <* {} *>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

              then 1 in ( dom <* {} *>) by TARSKI:def 1;

              

              then

               A58: (F . 1) = ( <* {} *> . 1) by FINSEQ_1:def 7

              .= {} by FINSEQ_1: 40;

              assume x in (F . n9);

              hence thesis by A57, A58;

            end;

          end;

            case

             A59: n9 <> 1;

            n9 in ( Seg ( len F)) by A56, FINSEQ_1:def 3;

            then 1 <= n9 by FINSEQ_1: 1;

            then 1 < n9 by A59, XXREAL_0: 1;

            then

             A60: (1 + 1) <= n9 by NAT_1: 13;

            thus for x be set st x in (F . n9) holds (f . x) = (a . n9)

            proof

              let x be set;

              assume

               A61: x in (F . n9);

              (F . n9) in ( rng F) by A56, FUNCT_1: 3;

              then (F . n9) in S;

              then

              reconsider x as Element of X by A61;

              (a . n9) = (f . x) by A41, A56, A60, A61;

              hence thesis;

            end;

          end;

        end;

        hence thesis;

      end;

      ( len F) = (( len <* {} *>) + ( len G)) by FINSEQ_1: 22

      .= (1 + ( len G)) by FINSEQ_1: 39;

      then 1 <= ( len F) by NAT_1: 11;

      then 1 in ( Seg ( len F)) by FINSEQ_1: 1;

      hence thesis by A23, A39, A40, A55, A44;

    end;

    

     Lm3: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st f is_simple_func_in S & f is nonnegative & (ex x be set st x in ( dom f) & 0. = (f . x)) holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st (F,a) are_Re-presentation_of f & (a . 1) = 0. & for n be Nat st 2 <= n & n in ( dom a) holds 0. < (a . n) & (a . n) < +infty

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      assume that

       A1: f is_simple_func_in S and

       A2: f is nonnegative and

       A3: ex x be set st x in ( dom f) & 0. = (f . x);

      

       a2: for x be object st x in ( dom f) holds 0. <= (f . x) by A2, SUPINF_2: 39;

      consider x0 be set such that

       A4: x0 in ( dom f) and

       A5: 0. = (f . x0) by A3;

      reconsider x0 as Element of X by A4;

      consider F1 be Finite_Sep_Sequence of S such that

       A6: ( dom f) = ( union ( rng F1)) and

       A7: for n be Nat, x,y be Element of X st n in ( dom F1) & x in (F1 . n) & y in (F1 . n) holds (f . x) = (f . y) by A1, MESFUNC2:def 4;

      consider V be set such that

       A8: x0 in V and

       A9: V in ( rng F1) by A4, A6, TARSKI:def 4;

      consider n0 be object such that

       A10: n0 in ( dom F1) and

       A11: V = (F1 . n0) by A9, FUNCT_1:def 3;

      set F0 = { Fn where Fn be Element of S : Fn in ( rng F1) & for x be Element of X st x in Fn holds (f . x) = 0. };

      set G1 = ( union F0);

      for F9 be object st F9 in F0 holds F9 in ( bool X)

      proof

        let F9 be object;

        assume F9 in F0;

        then ex Fn be Element of S st F9 = Fn & Fn in ( rng F1) & for x be Element of X st x in Fn holds (f . x) = 0. ;

        hence thesis;

      end;

      then

      reconsider F0 as Subset-Family of X by TARSKI:def 3;

      set N = { n where n be Element of NAT : n in ( dom F1) & for x be Element of X st x in (F1 . n) holds (f . x) = 0. };

      

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

      reconsider n0 as Element of NAT by A10;

      (F1 . n0) is Element of S & (F1 . n0) in ( rng F1) & for x be Element of X st x in (F1 . n0) holds (f . x) = 0.

      proof

        (F1 . n0) in ( rng F1) by A10, FUNCT_1: 3;

        hence (F1 . n0) is Element of S;

        thus (F1 . n0) in ( rng F1) by A10, FUNCT_1: 3;

        let x be Element of X;

        assume x in (F1 . n0);

        hence thesis by A5, A7, A8, A10, A11;

      end;

      then

       A13: (F1 . n0) in F0;

      for z be object st z in F0 holds z in ( rng F1)

      proof

        let z be object;

        assume z in F0;

        then ex Fn9 be Element of S st z = Fn9 & Fn9 in ( rng F1) & for x be Element of X st x in Fn9 holds (f . x) = 0. ;

        hence thesis;

      end;

      then

       A14: F0 c= ( rng F1);

      for z be object st z in N holds z in ( dom F1)

      proof

        let z be object;

        assume z in N;

        then ex n9 be Element of NAT st z = n9 & n9 in ( dom F1) & for x be Element of X st x in (F1 . n9) holds (f . x) = 0. ;

        hence thesis;

      end;

      then

       A15: N c= ( dom F1);

      then

      reconsider N as finite set;

      consider P1 be FinSequence such that

       A16: ( rng P1) = N & P1 is one-to-one by FINSEQ_4: 58;

      reconsider F0 as N_Sub_set_fam of X by A14, A13;

      for F9 be object st F9 in F0 holds F9 in S

      proof

        let F9 be object;

        assume F9 in F0;

        then ex Fn be Element of S st F9 = Fn & Fn in ( rng F1) & for x be Element of X st x in Fn holds (f . x) = 0. ;

        hence thesis;

      end;

      then F0 c= S;

      then

      reconsider G1 as Element of S by MEASURE1:def 5;

      

       A17: ( len P1) = ( card N) by A16, FINSEQ_4: 62;

      reconsider L = ( Seg ( len F1)) as finite set;

      set M = (( findom F1) \ N);

      consider P2 be FinSequence such that

       A18: ( rng P2) = M and

       A19: P2 is one-to-one by FINSEQ_4: 58;

      

       A20: N c= ( Seg ( len F1)) by A15, FINSEQ_1:def 3;

      then ( card N) <= ( card L) by NAT_1: 43;

      then ( len P1) <= ( len F1) by A17, FINSEQ_1: 57;

      then

      consider lenF be Nat such that

       A21: (( len F1) + 1) = (( len P1) + lenF) by A12, NAT_1: 10, XXREAL_0: 2;

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

      M = (( Seg ( len F1)) \ N) by FINSEQ_1:def 3;

      then

       A22: ( card M) = (( card ( Seg ( len F1))) - ( card N)) by A20, CARD_2: 44;

      defpred P[ Nat, set] means ($1 = 1 implies $2 = G1) & ($1 >= 2 implies ex k9 be Nat st k9 = ($1 - 1) & $2 = (F1 . (P2 . k9)));

      ( len P2) = ( card M) by A18, A19, FINSEQ_4: 62;

      then

       A23: ( len P2) = (((( len F1) - ( len P1)) + 1) - 1) by A17, A22, FINSEQ_1: 57;

      

       A24: for k be Nat st k in ( Seg lenF) holds ex U be Element of S st P[k, U]

      proof

        let k be Nat;

        assume

         A25: k in ( Seg lenF);

        per cases ;

          suppose

           A26: k = 1;

          take G1;

          thus thesis by A26;

        end;

          suppose

           A27: k <> 1;

          

           A28: k >= 1 by A25, FINSEQ_1: 1;

          then

          consider k9 be Nat such that

           A29: k = (1 + k9) by NAT_1: 10;

          k > 1 by A27, A28, XXREAL_0: 1;

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

          then

           A30: (k - 1) >= 1 by XREAL_1: 19;

          k <= lenF by A25, FINSEQ_1: 1;

          then (k - 1) <= (lenF - 1) by XREAL_1: 9;

          then k9 in ( Seg ( len P2)) by A21, A23, A29, A30, FINSEQ_1: 1;

          then k9 in ( dom P2) by FINSEQ_1:def 3;

          then (P2 . k9) in M by A18, FUNCT_1: 3;

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

          then

          reconsider U = (F1 . (P2 . k9)) as Element of S;

          take U;

          thus thesis by A27, A29;

        end;

      end;

      consider F be FinSequence of S such that

       A31: ( dom F) = ( Seg lenF) & for k be Nat st k in ( Seg lenF) holds P[k, (F . k)] from FINSEQ_1:sch 5( A24);

      defpred A[ Nat, Element of ExtREAL ] means for y be Element of X holds (y in (F . $1) implies $2 = (f . y)) & ((F . $1) = {} implies $2 = 1. );

      

       A32: for k be Nat st k in ( Seg ( len F)) holds ex x be Element of ExtREAL st A[k, x]

      proof

        let k be Nat;

        assume

         A33: k in ( Seg ( len F));

        then

         A34: k in ( dom F) by FINSEQ_1:def 3;

        now

          per cases ;

            case

             A35: k = 1;

            take x = 0. ;

            

             A36: (F . k) = G1 by A31, A34, A35;

            for y be Element of X holds (y in (F . k) implies 0. = (f . y)) & ((F . k) = {} implies 0. = 1. )

            proof

              let y be Element of X;

              y in (F . k) implies 0. = (f . y)

              proof

                assume y in (F . k);

                then

                consider Y be set such that

                 A37: y in Y and

                 A38: Y in F0 by A36, TARSKI:def 4;

                ex Fn be Element of S st Y = Fn & Fn in ( rng F1) & for x be Element of X st x in Fn holds (f . x) = 0. by A38;

                hence thesis by A37;

              end;

              hence thesis by A8, A11, A13, A36, TARSKI:def 4;

            end;

            hence thesis;

          end;

            case

             A39: k <> 1;

            1 <= k by A33, FINSEQ_1: 1;

            then 1 < k by A39, XXREAL_0: 1;

            then

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

            then

            consider k1 be Nat such that

             A41: k1 = (k - 1) and

             A42: (F . k) = (F1 . (P2 . k1)) by A31, A34;

            

             A43: 1 <= k1 by A40, A41, XREAL_1: 19;

            k <= lenF by A31, A34, FINSEQ_1: 1;

            then k1 <= ( len P2) by A21, A23, A41, XREAL_1: 9;

            then k1 in ( Seg ( len P2)) by A43, FINSEQ_1: 1;

            then k1 in ( dom P2) by FINSEQ_1:def 3;

            then (P2 . k1) in M by A18, FUNCT_1: 3;

            then

            consider k9 be set such that

             A44: k9 in ( dom F1) and

             A45: (F . k) = (F1 . k9) by A42;

            now

              per cases ;

                case

                 A46: (F . k) = {} ;

                take x = 1. ;

                for y be Element of X holds (y in (F . k) implies 1. = (f . y)) & ((F . k) = {} implies 1. = 1. ) by A46;

                hence thesis;

              end;

                case (F . k) <> {} ;

                then

                consider y1 be object such that

                 A47: y1 in (F . k) by XBOOLE_0:def 1;

                (F . k) in ( rng F) by A34, FUNCT_1: 3;

                then (F . k) in S;

                then

                reconsider y1 as Element of X by A47;

                take x = (f . y1);

                for y be Element of X holds (y in (F . k) implies x = (f . y)) & ((F . k) = {} implies x = 1. ) by A7, A44, A45, A47;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      consider a be FinSequence of ExtREAL such that

       A48: ( dom a) = ( Seg ( len F)) & for n be Nat st n in ( Seg ( len F)) holds A[n, (a . n)] from FINSEQ_1:sch 5( A32);

      

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

      proof

        let n be Nat;

        let x be Element of X;

        assume that

         A50: n in ( dom F) and

         A51: x in (F . n);

        n in ( Seg ( len F)) by A50, FINSEQ_1:def 3;

        hence thesis by A48, A51;

      end;

      

       A52: for n be Nat st n in ( dom F) holds for x be object st x in (F . n) holds (f . x) = (a . n)

      proof

        let n be Nat;

        assume

         A53: n in ( dom F);

        let x be object;

        assume

         A54: x in (F . n);

        (F . n) in ( rng F) by A53, FUNCT_1: 3;

        then (F . n) in S;

        then

        reconsider x as Element of X by A54;

        (a . n) = (f . x) by A49, A53, A54;

        hence thesis;

      end;

      

       A55: for x be Element of X st x in (F1 . n0) holds (f . x) = 0. by A5, A7, A8, A10, A11;

      

       A56: (a . 1) = 0. & ( dom F) = ( dom a) & for n be Nat, x be Element of X st n in ( dom F) & x in (F . n) holds (a . n) = (f . x)

      proof

        reconsider F1n0 = (F1 . n0) as Element of S by A9, A11;

        ( 0 + 1) <= lenF by A21, A23, XREAL_1: 19;

        then

         A57: 1 in ( Seg lenF) by FINSEQ_1: 1;

        then

         A58: 1 in ( Seg ( len F)) by A31, FINSEQ_1:def 3;

        

         A59: (F . 1) = G1 by A31, A57;

        F1n0 in F0 by A9, A11, A55;

        then x0 in (F . 1) by A8, A11, A59, TARSKI:def 4;

        hence (a . 1) = 0. by A5, A48, A58;

        thus ( dom F) = ( dom a) by A48, FINSEQ_1:def 3;

        thus thesis by A49;

      end;

      

       A60: for n,m be Nat st n in ( dom F) & m in ( dom F) & n = 1 & m <> 1 holds (F . n) misses (F . m)

      proof

        let n,m be Nat;

        assume that

         A61: n in ( dom F) and

         A62: m in ( dom F) and

         A63: n = 1 and

         A64: m <> 1;

        

         A65: (F . n) = G1 by A31, A61, A63;

        m <= lenF by A31, A62, FINSEQ_1: 1;

        then

         A66: (m - 1) <= (lenF - 1) by XREAL_1: 9;

        1 <= m by A62, FINSEQ_3: 25;

        then 1 < m by A64, XXREAL_0: 1;

        then

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

        then

        consider k9 be Nat such that

         A68: k9 = (m - 1) and

         A69: (F . m) = (F1 . (P2 . k9)) by A31, A62;

        (m - 1) >= 1 by A67, XREAL_1: 19;

        then k9 in ( Seg ( len P2)) by A21, A23, A68, A66, FINSEQ_1: 1;

        then k9 in ( dom P2) by FINSEQ_1:def 3;

        then

         A70: (P2 . k9) in M by A18, FUNCT_1: 3;

        then

         A71: not (P2 . k9) in N by XBOOLE_0:def 5;

        ((F . n) /\ (F . m)) = {}

        proof

          assume ((F . n) /\ (F . m)) <> {} ;

          then

          consider v be object such that

           A72: v in ((F . n) /\ (F . m)) by XBOOLE_0:def 1;

          

           A73: v in (F . m) by A72, XBOOLE_0:def 4;

          v in (F . n) by A72, XBOOLE_0:def 4;

          then

          consider Y be set such that

           A74: v in Y and

           A75: Y in F0 by A65, TARSKI:def 4;

          consider Fv be Element of S such that

           A76: Y = Fv and

           A77: Fv in ( rng F1) and

           A78: for x be Element of X st x in Fv holds (f . x) = 0. by A75;

          consider n9 be object such that

           A79: n9 in ( dom F1) and

           A80: Fv = (F1 . n9) by A77, FUNCT_1:def 3;

          reconsider n9 as Element of NAT by A79;

          n9 <> (P2 . k9) by A70, A71, A78, A80;

          then (F1 . n9) misses (F1 . (P2 . k9)) by PROB_2:def 2;

          then ((F1 . n9) /\ (F1 . (P2 . k9))) = {} ;

          hence contradiction by A69, A73, A74, A76, A80, XBOOLE_0:def 4;

        end;

        hence thesis;

      end;

      

       A81: for n,m be Nat st n in ( dom F) & m in ( dom F) & n <> 1 & m <> 1 & n <> m holds (F . n) misses (F . m)

      proof

        let n,m be Nat;

        assume that

         A82: n in ( dom F) and

         A83: m in ( dom F) and

         A84: n <> 1 and

         A85: m <> 1 and

         A86: n <> m;

        n <= lenF by A31, A82, FINSEQ_1: 1;

        then

         A87: (n - 1) <= (lenF - 1) by XREAL_1: 9;

        m <= lenF by A31, A83, FINSEQ_1: 1;

        then

         A88: (m - 1) <= (lenF - 1) by XREAL_1: 9;

        1 <= m by A31, A83, FINSEQ_1: 1;

        then 1 < m by A85, XXREAL_0: 1;

        then

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

        then

        consider k2 be Nat such that

         A90: k2 = (m - 1) and

         A91: (F . m) = (F1 . (P2 . k2)) by A31, A83;

        1 <= (m - 1) by A89, XREAL_1: 19;

        then k2 in ( Seg ( len P2)) by A21, A23, A90, A88, FINSEQ_1: 1;

        then

         A92: k2 in ( dom P2) by FINSEQ_1:def 3;

        1 <= n by A31, A82, FINSEQ_1: 1;

        then 1 < n by A84, XXREAL_0: 1;

        then

         A93: (1 + 1) <= n by NAT_1: 13;

        then

        consider k1 be Nat such that

         A94: k1 = (n - 1) and

         A95: (F . n) = (F1 . (P2 . k1)) by A31, A82;

        1 <= (n - 1) by A93, XREAL_1: 19;

        then k1 in ( Seg ( len P2)) by A21, A23, A94, A87, FINSEQ_1: 1;

        then

         A96: k1 in ( dom P2) by FINSEQ_1:def 3;

        k1 <> k2 by A86, A94, A90;

        then (P2 . k1) <> (P2 . k2) by A19, A96, A92, FUNCT_1:def 4;

        hence thesis by A95, A91, PROB_2:def 2;

      end;

      

       A97: for x,y be object st x <> y holds (F . x) misses (F . y)

      proof

        let x,y be object;

        assume

         A98: x <> y;

        now

          per cases ;

            case

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

            then

            reconsider x, y as Element of NAT ;

            now

              per cases ;

                case x = 1 or y = 1;

                hence thesis by A60, A98, A99;

              end;

                case x <> 1 & y <> 1;

                hence thesis by A81, A98, A99;

              end;

            end;

            hence thesis;

          end;

            case

             A100: not x in ( dom F) or not y in ( dom F);

            now

              per cases by A100;

                case not x in ( dom F);

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

                hence thesis;

              end;

                case not y in ( dom F);

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

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      for z be object st z in ( union ( rng F)) holds z in ( union ( rng F1))

      proof

        let z be object;

        assume z in ( union ( rng F));

        then

        consider Y be set such that

         A101: z in Y and

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

        consider k be object such that

         A103: k in ( dom F) and

         A104: Y = (F . k) by A102, FUNCT_1:def 3;

        reconsider k as Element of NAT by A103;

        now

          per cases ;

            case k = 1;

            then z in G1 by A31, A101, A103, A104;

            then

            consider Y9 be set such that

             A105: z in Y9 and

             A106: Y9 in F0 by TARSKI:def 4;

            ex Fn9 be Element of S st Y9 = Fn9 & Fn9 in ( rng F1) & for x be Element of X st x in Fn9 holds (f . x) = 0. by A106;

            hence thesis by A105, TARSKI:def 4;

          end;

            case

             A107: k <> 1;

            1 <= k by A31, A103, FINSEQ_1: 1;

            then 1 < k by A107, XXREAL_0: 1;

            then

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

            then

            consider k9 be Nat such that

             A109: k9 = (k - 1) and

             A110: (F . k) = (F1 . (P2 . k9)) by A31, A103;

            

             A111: 1 <= k9 by A108, A109, XREAL_1: 19;

            k <= lenF by A31, A103, FINSEQ_1: 1;

            then k9 <= ( len P2) by A21, A23, A109, XREAL_1: 9;

            then k9 in ( dom P2) by A111, FINSEQ_3: 25;

            then (P2 . k9) in M by A18, FUNCT_1: 3;

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

            hence thesis by A101, A104, A110, TARSKI:def 4;

          end;

        end;

        hence thesis;

      end;

      then

       A112: ( union ( rng F)) c= ( union ( rng F1));

      for z be object st z in ( union ( rng F1)) holds z in ( union ( rng F))

      proof

        let z be object;

        assume z in ( union ( rng F1));

        then

        consider Y be set such that

         A113: z in Y and

         A114: Y in ( rng F1) by TARSKI:def 4;

        consider m1 be object such that

         A115: m1 in ( dom F1) and

         A116: Y = (F1 . m1) by A114, FUNCT_1:def 3;

        reconsider m1 as Element of NAT by A115;

        now

          per cases ;

            case m1 in N;

            then ex m19 be Element of NAT st m1 = m19 & m19 in ( dom F1) & for x be Element of X st x in (F1 . m19) holds (f . x) = 0. ;

            then Y in F0 by A114, A116;

            then

             A117: z in ( union F0) by A113, TARSKI:def 4;

            lenF >= (1 + 0 ) by A21, A23, XREAL_1: 19;

            then

             A118: 1 in ( Seg lenF) by FINSEQ_1: 1;

            then (F . 1) in ( rng F) by A31, FUNCT_1: 3;

            then ( union F0) in ( rng F) by A31, A118;

            hence thesis by A117, TARSKI:def 4;

          end;

            case not m1 in N;

            then m1 in M by A115, XBOOLE_0:def 5;

            then

            consider m19 be object such that

             A119: m19 in ( dom P2) and

             A120: m1 = (P2 . m19) by A18, FUNCT_1:def 3;

            reconsider m19 as Element of NAT by A119;

            

             A121: m19 in ( Seg ( len P2)) by A119, FINSEQ_1:def 3;

            then m19 <= ( len P2) by FINSEQ_1: 1;

            then

             A122: (m19 + 1) <= lenF by A21, A23, XREAL_1: 6;

            reconsider m2 = (m19 + 1) as Nat;

            1 <= m19 by A121, FINSEQ_1: 1;

            then

             A123: (1 + 1) <= (m19 + 1) by XREAL_1: 6;

            then 1 <= m2 by XXREAL_0: 2;

            then

             A124: m2 in ( Seg lenF) by A122, FINSEQ_1: 1;

            then

             A125: (F . m2) in ( rng F) by A31, FUNCT_1: 3;

            ex k9 be Nat st k9 = (m2 - 1) & (F . m2) = (F1 . (P2 . k9)) by A31, A123, A124;

            hence thesis by A113, A116, A120, A125, TARSKI:def 4;

          end;

        end;

        hence thesis;

      end;

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

      then

       A126: ( union ( rng F)) = ( dom f) by A6, A112;

      reconsider F as Finite_Sep_Sequence of S by A97, PROB_2:def 2;

      take F, a;

      for n be Nat st 2 <= n & n in ( dom a) holds 0. < (a . n) & (a . n) < +infty

      proof

        

         A127: f is real-valued by A1, MESFUNC2:def 4;

        ( 0 + 1) <= lenF by A21, A23, XREAL_1: 19;

        then

         A128: 1 in ( dom F) by A31, FINSEQ_1: 1;

        let n be Nat;

        assume that

         A129: 2 <= n and

         A130: n in ( dom a);

        (1 + 1) <= n by A129;

        then

         A131: 1 <= (n - 1) by XREAL_1: 19;

        consider k1 be Nat such that

         A132: k1 = (n - 1) and

         A133: (F . n) = (F1 . (P2 . k1)) by A31, A56, A129, A130;

        n <= lenF by A31, A56, A130, FINSEQ_1: 1;

        then (n - 1) <= (lenF - 1) by XREAL_1: 9;

        then k1 in ( Seg ( len P2)) by A21, A23, A132, A131, FINSEQ_1: 1;

        then k1 in ( dom P2) by FINSEQ_1:def 3;

        then (P2 . k1) in M by A18, FUNCT_1: 3;

        then

         A134: (F . n) in ( rng F1) by A133, FUNCT_1: 3;

        n <> 1 by A129;

        then (F . 1) misses (F . n) by A56, A60, A130, A128;

        then

         A135: G1 misses (F . n) by A31, A128;

        (a . n) <> 0. & 0. <= (a . n) & (a . n) < +infty

        proof

          per cases ;

            suppose

             A136: (F . n) <> {} ;

            

             A137: (F . n) in ( rng F) by A56, A130, FUNCT_1: 3;

            then

            reconsider Fn = (F . n) as Element of S;

            consider y be object such that

             A138: y in (F . n) by A136, XBOOLE_0:def 1;

            (F . n) in S by A137;

            then

            reconsider y as Element of X by A138;

            

             A139: (a . n) = (f . y) by A48, A130, A138;

            (G1 /\ (F . n)) = {} by A135;

            then

             A140: not y in G1 by A138, XBOOLE_0:def 4;

            thus (a . n) <> 0.

            proof

              assume (a . n) = 0. ;

              then for x be Element of X st x in (F . n) holds (f . x) = 0. by A56, A130;

              then Fn in F0 by A134;

              hence contradiction by A138, A140, TARSKI:def 4;

            end;

            

             A141: y in ( union ( rng F)) by A138, A137, TARSKI:def 4;

            then |.(f . y).| < +infty by A6, A112, A127, MESFUNC2:def 1;

            hence thesis by A6, A112, A139, A141, EXTREAL1: 21, a2;

          end;

            suppose

             A142: (F . n) = {} ;

            hence (a . n) <> 0. by A48, A130;

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

            thus 0. <= (a . n) by A48, A130, A142;

             A[n, (a . n)] by A48, A130;

            then (a . n) = jj by A142;

            hence (a . n) < +infty by XXREAL_0: 9;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A126, A56, A52;

    end;

    theorem :: MESFUNC3:14

    

     Th14: for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL st f is_simple_func_in S & f is nonnegative holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st (F,a) are_Re-presentation_of f & (a . 1) = 0. & for n be Nat st 2 <= n & n in ( dom a) holds 0. < (a . n) & (a . n) < +infty

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      assume

       A1: f is_simple_func_in S & f is nonnegative;

      per cases ;

        suppose ex x be object st x in ( dom f) & 0. = (f . x);

        hence thesis by A1, Lm3;

      end;

        suppose for x be object st x in ( dom f) holds 0. <> (f . x);

        hence thesis by A1, Lm2;

      end;

    end;

    theorem :: MESFUNC3:15

    for X be non empty set, S be SigmaField of X, f be PartFunc of X, ExtREAL , F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL , x be Element of X st (F,a) are_Re-presentation_of f & x in ( dom f) holds ex ax be FinSequence of ExtREAL st ( dom ax) = ( dom a) & (for n be Nat st n in ( dom ax) holds (ax . n) = ((a . n) * (( chi ((F . n),X)) . x))) & (f . x) = ( Sum ax)

    proof

      let X be non empty set;

      let S be SigmaField of X;

      let f be PartFunc of X, ExtREAL ;

      let F be Finite_Sep_Sequence of S;

      let a be FinSequence of ExtREAL ;

      let x be Element of X such that

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

       A2: x in ( dom f);

      

       A3: ( dom F) = ( dom a) by A1;

      deffunc F( Nat) = ((a . $1) * (( chi ((F . $1),X)) . x));

      consider ax be FinSequence of ExtREAL such that

       A4: ( len ax) = ( len a) & for j be Nat st j in ( dom ax) holds (ax . j) = F(j) from FINSEQ_2:sch 1;

      

       A5: ( dom ax) = ( Seg ( len a)) by A4, FINSEQ_1:def 3;

      

       A6: ( dom f) = ( union ( rng F)) by A1;

      

       A7: (f . x) = ( Sum ax)

      proof

        consider Y be set such that

         A8: x in Y and

         A9: Y in ( rng F) by A2, A6, TARSKI:def 4;

        consider k be object such that

         A10: k in ( dom F) and

         A11: Y = (F . k) by A9, FUNCT_1:def 3;

        reconsider k as Element of NAT by A10;

        

         A12: k in ( Seg ( len a)) by A3, A10, FINSEQ_1:def 3;

        then

         A13: ( len ax) >= k by A4, FINSEQ_1: 1;

        

         A14: for i be Nat st i in ( Seg ( len ax)) & i <> k holds (ax . i) = 0.

        proof

          let i be Nat;

          assume that

           A15: i in ( Seg ( len ax)) and

           A16: i <> k;

          (F . i) misses (F . k) by A16, PROB_2:def 2;

          then ((F . i) /\ (F . k)) = {} ;

          then not x in (F . i) by A8, A11, XBOOLE_0:def 4;

          then

           A17: (( chi ((F . i),X)) . x) = 0. by FUNCT_3:def 3;

          (ax . i) = ((a . i) * (( chi ((F . i),X)) . x)) by A4, A5, A15;

          hence thesis by A17;

        end;

        consider SA be sequence of ExtREAL such that

         A18: ( Sum ax) = (SA . ( len ax)) and

         A19: (SA . 0 ) = 0. and

         A20: for i be Nat st i < ( len ax) holds (SA . (i + 1)) = ((SA . i) + (ax . (i + 1))) by EXTREAL1:def 2;

        defpred P[ Nat] means $1 <= ( len ax) implies ($1 < k implies (SA . $1) = 0. ) & ($1 >= k implies (SA . $1) = (f . x));

        

         A21: for i be Nat st i in ( Seg ( len ax)) & i = k holds (ax . i) = (f . x)

        proof

          let i be Nat;

          assume that

           A22: i in ( Seg ( len ax)) and

           A23: i = k;

          (( chi ((F . i),X)) . x) = 1. by A8, A11, A23, FUNCT_3:def 3;

          

          then (ax . i) = ((a . i) * 1. ) by A4, A5, A22

          .= (a . i) by XXREAL_3: 81;

          hence thesis by A1, A8, A10, A11, A23;

        end;

        

         A24: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let i be Nat;

          assume

           A25: P[i];

          assume

           A26: (i + 1) <= ( len ax);

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

          now

            per cases ;

              case

               A27: (i + 1) < k;

              

               A28: k <= ( len a) by A12, FINSEQ_1: 1;

              

               A29: i <= (i + 1) by NAT_1: 11;

              then i < k by A27, XXREAL_0: 2;

              then

               A30: i < ( len ax) by A4, A28, XXREAL_0: 2;

              then 1 <= (i + 1) & (i + 1) <= ( len ax) by NAT_1: 11, NAT_1: 13;

              then

               A31: (i + 1) in ( Seg ( len ax)) by FINSEQ_1: 1;

              (SA . (i + 1)) = ( 0. + (ax . (i + 1))) by A20, A25, A27, A29, A30, XXREAL_0: 2

              .= (ax . (i + 1)) by XXREAL_3: 4

              .= 0. by A14, A27, A31;

              hence thesis by A27;

            end;

              case

               A32: (i + 1) >= k;

              now

                per cases ;

                  case

                   A33: k = (i + 1);

                  

                   A34: k <= ( len a) by A12, FINSEQ_1: 1;

                  then i < ( len ax) by A4, A33, NAT_1: 13;

                  

                  hence (SA . (i + 1)) = ((SA . i) + (ax . (i + 1))) by A20

                  .= (ax . k) by A4, A25, A33, A34, NAT_1: 13, XXREAL_3: 4

                  .= (f . x) by A4, A12, A21;

                end;

                  case k <> (i + 1);

                  then

                   A35: k < (i + 1) by A32, XXREAL_0: 1;

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

                  then

                   A36: (i + 1) in ( Seg ( len ax)) by A26, FINSEQ_1: 1;

                  i < ( len ax) by A26, NAT_1: 13;

                  

                  hence (SA . (i + 1)) = ((SA . i) + (ax . (i + 1))) by A20

                  .= ((f . x) + 0. ) by A14, A25, A26, A35, A36, NAT_1: 13

                  .= (f . x) by XXREAL_3: 4;

                end;

              end;

              hence thesis by A32;

            end;

          end;

          hence thesis;

        end;

        

         A37: P[ 0 ] by A12, A19, FINSEQ_1: 1;

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

        hence thesis by A18, A13;

      end;

      take ax;

      ( dom ax) = ( Seg ( len a)) by A4, FINSEQ_1:def 3;

      hence thesis by A4, A7, FINSEQ_1:def 3;

    end;

    theorem :: MESFUNC3:16

    for p be FinSequence of ExtREAL , q be FinSequence of REAL st p = q holds ( Sum p) = ( Sum q) by Th2;

    theorem :: MESFUNC3:17

    

     Th17: for p be FinSequence of ExtREAL st not -infty in ( rng p) & +infty in ( rng p) holds ( Sum p) = +infty

    proof

      let p be FinSequence of ExtREAL ;

      assume

       A1: not -infty in ( rng p);

      assume +infty in ( rng p);

      then ex n be object st n in ( dom p) & (p . n) = +infty by FUNCT_1:def 3;

      then

      consider m be Nat such that

       A2: m in ( dom p) and

       A3: (p . m) = +infty ;

      m in ( Seg ( len p)) by A2, FINSEQ_1:def 3;

      then

       A4: ( len p) >= m by FINSEQ_1: 1;

      consider f be sequence of ExtREAL such that

       A5: ( Sum p) = (f . ( len p)) and

       A6: (f . 0 ) = 0. and

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

      

       A8: for n be Nat st n in ( dom p) holds -infty < (p . n)

      proof

        let n be Nat;

        assume n in ( dom p);

        then (p . n) in ( rng p) by FUNCT_1:def 3;

        hence thesis by A1, XXREAL_0: 6;

      end;

      defpred P[ Nat] means $1 <= ( len p) implies ($1 < m implies -infty < (f . $1)) & ($1 >= m implies (f . $1) = +infty );

      

       A9: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A10: P[i];

        assume

         A11: (i + 1) <= ( len p);

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

        

         A12: i < ( len p) by A11, NAT_1: 13;

        now

          per cases ;

            case (i + 1) < m;

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

            then (i + 1) in ( Seg ( len p)) by A11, FINSEQ_1: 1;

            then (i + 1) in ( dom p) by FINSEQ_1:def 3;

            then

             A13: -infty < (p . (i + 1)) by A8;

            

             A14: ( -infty + -infty ) = -infty by XXREAL_3:def 2;

            ( -infty + -infty ) < ((f . i) + (p . (i + 1))) by A10, A11, A13, NAT_1: 13, XXREAL_3: 64;

            hence -infty < (f . (i + 1)) by A7, A12, A14;

          end;

            case

             A15: (i + 1) >= m;

            now

              per cases ;

                case

                 A16: (i + 1) = m;

                (f . (i + 1)) = ((f . i) + (p . (i + 1))) by A7, A12;

                hence (f . (i + 1)) = +infty by A3, A10, A11, A16, NAT_1: 13, XXREAL_3:def 2;

              end;

                case

                 A17: (i + 1) <> m;

                i < ( len p) by A11, NAT_1: 13;

                then

                 A18: (f . (i + 1)) = ((f . i) + (p . (i + 1))) by A7;

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

                then (i + 1) in ( Seg ( len p)) by A11, FINSEQ_1: 1;

                then (i + 1) in ( dom p) by FINSEQ_1:def 3;

                then

                 A19: (p . (i + 1)) <> -infty by A8;

                (i + 1) > m by A15, A17, XXREAL_0: 1;

                hence (f . (i + 1)) = +infty by A10, A11, A19, A18, NAT_1: 13, XXREAL_3:def 2;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A20: P[ 0 ] by A2, A6, FINSEQ_3: 25;

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

      hence thesis by A5, A4;

    end;

    definition

      let X be non empty set;

      let S be SigmaField of X;

      let M be sigma_Measure of S;

      let f be PartFunc of X, ExtREAL ;

      assume

       A1: f is_simple_func_in S & f is nonnegative;

      :: MESFUNC3:def2

      func integral (M,f) -> Element of ExtREAL means ex F be Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL st (F,a) are_Re-presentation_of f & (a . 1) = 0. & (for n be Nat st 2 <= n & n in ( dom a) holds 0. < (a . n) & (a . n) < +infty ) & ( dom x) = ( dom F) & (for n be Nat st n in ( dom x) holds (x . n) = ((a . n) * ((M * F) . n))) & it = ( Sum x);

      existence

      proof

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

         A2: (F,a) are_Re-presentation_of f & (a . 1) = 0. & for n be Nat st 2 <= n & n in ( dom a) holds 0. < (a . n) & (a . n) < +infty by A1, Th14;

        defpred P[ object] means $1 in ( dom F);

        deffunc G( object) = ((a . $1) * ((M * F) . $1));

        

         A3: for x be object st P[x] holds G(x) in ExtREAL by XXREAL_0:def 1;

        consider p be PartFunc of NAT , ExtREAL such that

         A4: (for x be object holds x in ( dom p) iff x in NAT & P[x]) & for x be object st x in ( dom p) holds (p . x) = G(x) from PARTFUN1:sch 3( A3);

        for x be object st x in ( dom F) holds x in ( dom p) by A4;

        then

         A5: ( dom F) c= ( dom p);

        for x be object st x in ( dom p) holds x in ( dom F) by A4;

        then ( dom p) c= ( dom F);

        then

         A6: ( dom p) = ( dom F) by A5;

        then ( dom p) = ( Seg ( len F)) by FINSEQ_1:def 3;

        then

         A7: p is FinSequence by FINSEQ_1:def 2;

        ( rng p) c= ExtREAL ;

        then

        reconsider p as FinSequence of ExtREAL by A7, FINSEQ_1:def 4;

        take ( Sum p);

        for n be Nat st n in ( dom p) holds (p . n) = ((a . n) * ((M * F) . n)) by A4;

        hence thesis by A2, A6;

      end;

      uniqueness

      proof

        let s1,s2 be Element of ExtREAL such that

         A8: ex F1 be Finite_Sep_Sequence of S, a1,x1 be FinSequence of ExtREAL st (F1,a1) are_Re-presentation_of f & (a1 . 1) = 0. & (for n be Nat st 2 <= n & n in ( dom a1) holds 0. < (a1 . n) & (a1 . n) < +infty ) & ( dom x1) = ( dom F1) & (for n be Nat st n in ( dom x1) holds (x1 . n) = ((a1 . n) * ((M * F1) . n))) & s1 = ( Sum x1) and

         A9: ex F2 be Finite_Sep_Sequence of S, a2 be FinSequence of ExtREAL , x2 be FinSequence of ExtREAL st (F2,a2) are_Re-presentation_of f & (a2 . 1) = 0. & (for n be Nat st 2 <= n & n in ( dom a2) holds 0. < (a2 . n) & (a2 . n) < +infty ) & ( dom x2) = ( dom F2) & (for n be Nat st n in ( dom x2) holds (x2 . n) = ((a2 . n) * ((M * F2) . n))) & s2 = ( Sum x2);

        thus s1 = s2

        proof

          consider F2 be Finite_Sep_Sequence of S, a2 be FinSequence of ExtREAL , x2 be FinSequence of ExtREAL such that

           A10: (F2,a2) are_Re-presentation_of f and

           A11: (a2 . 1) = 0. and

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

           A13: ( dom x2) = ( dom F2) and

           A14: for n be Nat st n in ( dom x2) holds (x2 . n) = ((a2 . n) * ((M * F2) . n)) and

           A15: s2 = ( Sum x2) by A9;

          

           A16: ( dom F2) = ( dom a2) by A10;

          

           A17: for n be Nat st n in ( dom a2) holds 0. <= (a2 . n)

          proof

            let n be Nat;

            assume

             A18: n in ( dom a2);

            now

              per cases ;

                case n = 1;

                thus (a2 . 1) = 0. by A11;

              end;

                case

                 A19: n <> 1;

                n in ( Seg ( len a2)) by A18, FINSEQ_1:def 3;

                then 1 <= n by FINSEQ_1: 1;

                then 1 < n by A19, XXREAL_0: 1;

                then (1 + 1) < (n + 1) by XREAL_1: 8;

                then 2 <= n by NAT_1: 13;

                hence thesis by A12, A18;

              end;

            end;

            hence thesis;

          end;

          

           A20: for n be Nat st n in ( dom F2) holds 0. <= ((M * F2) . n)

          proof

            let n be Nat;

            assume n in ( dom F2);

            then ((M * F2) . n) = (M . (F2 . n)) & (F2 . n) in ( rng F2) by FUNCT_1: 3, FUNCT_1: 13;

            hence thesis by SUPINF_2: 39;

          end;

          

           A21: not -infty in ( rng x2)

          proof

            assume not thesis;

            then

            consider n be object such that

             A22: n in ( dom x2) and

             A23: (x2 . n) = -infty by FUNCT_1:def 3;

            reconsider n as set by TARSKI: 1;

             0. <= (a2 . n) & 0. <= ((M * F2) . n) by A13, A16, A20, A17, A22;

            then 0. <= ((a2 . n) * ((M * F2) . n));

            hence thesis by A14, A22, A23;

          end;

          consider F1 be Finite_Sep_Sequence of S, a1 be FinSequence of ExtREAL , x1 be FinSequence of ExtREAL such that

           A24: (F1,a1) are_Re-presentation_of f and

           A25: (a1 . 1) = 0. and

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

           A27: ( dom x1) = ( dom F1) and

           A28: for n be Nat st n in ( dom x1) holds (x1 . n) = ((a1 . n) * ((M * F1) . n)) and

           A29: s1 = ( Sum x1) by A8;

          

           A30: ( dom F1) = ( dom a1) by A24;

          

           A31: for n be Nat st n in ( dom a1) holds 0. <= (a1 . n)

          proof

            let n be Nat;

            assume

             A32: n in ( dom a1);

            now

              per cases ;

                case n = 1;

                thus (a1 . 1) = 0. by A25;

              end;

                case

                 A33: n <> 1;

                n in ( Seg ( len a1)) by A32, FINSEQ_1:def 3;

                then 1 <= n by FINSEQ_1: 1;

                then 1 < n by A33, XXREAL_0: 1;

                then (1 + 1) < (n + 1) by XREAL_1: 8;

                then 2 <= n by NAT_1: 13;

                hence thesis by A26, A32;

              end;

            end;

            hence thesis;

          end;

          

           A34: for n be Nat st n in ( dom F1) holds 0. <= ((M * F1) . n)

          proof

            let n be Nat;

            assume n in ( dom F1);

            then ((M * F1) . n) = (M . (F1 . n)) & (F1 . n) in ( rng F1) by FUNCT_1: 3, FUNCT_1: 13;

            hence thesis by SUPINF_2: 39;

          end;

          

           A35: not -infty in ( rng x1)

          proof

            assume not thesis;

            then

            consider n be object such that

             A36: n in ( dom x1) and

             A37: (x1 . n) = -infty by FUNCT_1:def 3;

            reconsider n as set by TARSKI: 1;

             0. <= (a1 . n) & 0. <= ((M * F1) . n) by A27, A30, A34, A31, A36;

            then 0. <= ((a1 . n) * ((M * F1) . n));

            hence thesis by A28, A36, A37;

          end;

          now

            per cases ;

              case ex i,j be Nat st i in ( dom F1) & j in ( dom F2) & 2 <= i & 2 <= j & (M . ((F1 . i) /\ (F2 . j))) = +infty ;

              then

              consider i,j be Nat such that

               A38: i in ( dom F1) and

               A39: j in ( dom F2) and

               A40: 2 <= i and

               A41: 2 <= j and

               A42: (M . ((F1 . i) /\ (F2 . j))) = +infty ;

              

               A43: (F2 . j) in ( rng F2) by A39, FUNCT_1: 3;

              

               A44: (F1 . i) in ( rng F1) by A38, FUNCT_1: 3;

              then

               A45: ((F1 . i) /\ (F2 . j)) in S by A43, MEASURE1: 34;

              ((F1 . i) /\ (F2 . j)) c= (F1 . i) by XBOOLE_1: 17;

              then (M . (F1 . i)) = +infty by A42, A44, A45, MEASURE1: 31, XXREAL_0: 4;

              then

               A46: ((M * F1) . i) = +infty by A38, FUNCT_1: 13;

               0. < (a1 . i) by A26, A30, A38, A40;

              then +infty = ((a1 . i) * ((M * F1) . i)) by A46, XXREAL_3:def 5;

              then (x1 . i) = +infty by A27, A28, A38;

              then +infty in ( rng x1) by A27, A38, FUNCT_1:def 3;

              then

               A47: ( Sum x1) = +infty by A35, Th17;

              ((F1 . i) /\ (F2 . j)) c= (F2 . j) by XBOOLE_1: 17;

              then (M . (F2 . j)) = +infty by A42, A43, A45, MEASURE1: 31, XXREAL_0: 4;

              then

               A48: ((M * F2) . j) = +infty by A39, FUNCT_1: 13;

               0. < (a2 . j) by A12, A16, A39, A41;

              then +infty = ((a2 . j) * ((M * F2) . j)) by A48, XXREAL_3:def 5;

              then (x2 . j) = +infty by A13, A14, A39;

              then +infty in ( rng x2) by A13, A39, FUNCT_1:def 3;

              hence thesis by A29, A15, A21, A47, Th17;

            end;

              case

               A49: for i,j be Nat st i in ( dom F1) & j in ( dom F2) & 2 <= i & 2 <= j holds (M . ((F1 . i) /\ (F2 . j))) <> +infty ;

              set m = ( len x2);

              set n = ( len x1);

              ex a be Function of [:( Seg n), ( Seg m):], REAL st for i,j be Nat st i in ( Seg n) & j in ( Seg m) holds (a . (i,j)) = ((a1 . i) * (M . ((F1 . i) /\ (F2 . j))))

              proof

                deffunc F( object, object) = ((a1 . $1) * (M . ((F1 . $1) /\ (F2 . $2))));

                

                 A50: for x,y be object st x in ( Seg n) & y in ( Seg m) holds F(x,y) in REAL

                proof

                  let x,y be object such that

                   A51: x in ( Seg n) and

                   A52: y in ( Seg m);

                  x in { k where k be Nat : 1 <= k & k <= n } by A51, FINSEQ_1:def 1;

                  then

                  consider kx be Nat such that

                   A53: x = kx and

                   A54: 1 <= kx and kx <= n;

                  y in { k where k be Nat : 1 <= k & k <= m } by A52, FINSEQ_1:def 1;

                  then

                  consider ky be Nat such that

                   A55: y = ky and

                   A56: 1 <= ky and ky <= m;

                  

                   A57: ky in ( dom F2) by A13, A52, A55, FINSEQ_1:def 3;

                  then

                   A58: (F2 . ky) in ( rng F2) by FUNCT_1: 3;

                  

                   A59: kx in ( dom F1) by A27, A51, A53, FINSEQ_1:def 3;

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

                  then

                   A60: ((F1 . kx) /\ (F2 . ky)) in S by A58, MEASURE1: 34;

                  now

                    per cases ;

                      case

                       A61: not (2 <= kx & 2 <= ky);

                      now

                        per cases by A61;

                          case

                           A62: kx < 2;

                          then kx <= (1 + 1);

                          then kx <= 1 by A62, NAT_1: 8;

                          

                          then F(kx,ky) = ( 0. * (M . ((F1 . kx) /\ (F2 . ky)))) by A25, A54, XXREAL_0: 1

                          .= 0 ;

                          hence F(kx,ky) in REAL by XREAL_0:def 1;

                        end;

                          case

                           A63: ky < 2;

                          then ky <= (1 + 1);

                          then

                           A64: ky <= 1 by A63, NAT_1: 8;

                          now

                            per cases ;

                              case ((F1 . kx) /\ (F2 . ky)) = {} ;

                              

                              hence F(kx,ky) = ((a1 . kx) * 0. ) by VALUED_0:def 19

                              .= 0 ;

                            end;

                              case ((F1 . kx) /\ (F2 . ky)) <> {} ;

                              then

                              consider x be object such that

                               A65: x in ((F1 . kx) /\ (F2 . ky)) by XBOOLE_0:def 1;

                              

                               A66: x in (F2 . ky) by A65, XBOOLE_0:def 4;

                              x in (F1 . kx) by A65, XBOOLE_0:def 4;

                              

                              then (a1 . kx) = (f . x) by A24, A59

                              .= (a2 . ky) by A10, A57, A66

                              .= 0. by A11, A56, A64, XXREAL_0: 1;

                              hence F(kx,ky) = 0 ;

                            end;

                          end;

                          hence F(kx,ky) in REAL by XREAL_0:def 1;

                        end;

                      end;

                      hence F(kx,ky) in REAL ;

                    end;

                      case

                       A67: 2 <= kx & 2 <= ky;

                      

                       A68: 0. <= (a1 . kx) by A30, A31, A59;

                      (a1 . kx) <> +infty by A26, A30, A59, A67;

                      then

                      reconsider r2 = (a1 . kx) as Element of REAL by A68, XXREAL_0: 14;

                       0. <= (M . ((F1 . kx) /\ (F2 . ky))) by A60, SUPINF_2: 39;

                      then

                      reconsider r3 = (M . ((F1 . kx) /\ (F2 . ky))) as Element of REAL by A49, A59, A57, A67, XXREAL_0: 14;

                      ((a1 . kx) * (M . ((F1 . kx) /\ (F2 . ky)))) = (r2 * r3) by EXTREAL1: 1;

                      hence F(kx,ky) in REAL by XREAL_0:def 1;

                    end;

                  end;

                  hence thesis by A53, A55;

                end;

                consider f be Function of [:( Seg n), ( Seg m):], REAL such that

                 A69: for x,y be object st x in ( Seg n) & y in ( Seg m) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 2( A50);

                take f;

                thus thesis by A69;

              end;

              then

              consider a be Function of [:( Seg n), ( Seg m):], REAL such that

               A70: for i,j be Nat st i in ( Seg n) & j in ( Seg m) holds (a . (i,j)) = ((a1 . i) * (M . ((F1 . i) /\ (F2 . j))));

              ex p be FinSequence of REAL st ( dom p) = ( Seg n) & for i be Nat st i in ( dom p) holds ex r be FinSequence of REAL st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . [i, j]))

              proof

                defpred P[ Nat, object] means ex r be FinSequence of REAL st ( dom r) = ( Seg m) & $2 = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . [$1, j]);

                

                 A71: for k be Nat st k in ( Seg n) holds ex x be object st P[k, x]

                proof

                  let k be Nat;

                  assume k in ( Seg n);

                  deffunc G( set) = (a . [k, $1]);

                  consider r be FinSequence such that

                   A72: ( len r) = m and

                   A73: for i be Nat st i in ( dom r) holds (r . i) = G(i) from FINSEQ_1:sch 2;

                  

                   A74: ( dom r) = ( Seg m) by A72, FINSEQ_1:def 3;

                  for i be Nat st i in ( dom r) holds (r . i) in REAL

                  proof

                    let i be Nat;

                    

                     A75: (a . [k, i]) in REAL by XREAL_0:def 1;

                    assume i in ( dom r);

                    hence thesis by A73, A75;

                  end;

                  then

                  reconsider r as FinSequence of REAL by FINSEQ_2: 12;

                  take x = ( Sum r);

                  thus thesis by A73, A74;

                end;

                consider p be FinSequence such that

                 A76: ( dom p) = ( Seg n) & for k be Nat st k in ( Seg n) holds P[k, (p . k)] from FINSEQ_1:sch 1( A71);

                for i be Nat st i in ( dom p) holds (p . i) in REAL

                proof

                  let i be Nat;

                  assume i in ( dom p);

                  then ex r be FinSequence of REAL st ( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . [i, j]) by A76;

                  hence thesis by XREAL_0:def 1;

                end;

                then

                reconsider p as FinSequence of REAL by FINSEQ_2: 12;

                take p;

                thus thesis by A76;

              end;

              then

              consider p be FinSequence of REAL such that

               A77: ( dom p) = ( Seg n) and

               A78: for i be Nat st i in ( dom p) holds ex r be FinSequence of REAL st (( dom r) = ( Seg m) & (p . i) = ( Sum r) & for j be Nat st j in ( dom r) holds (r . j) = (a . [i, j]));

              

               A79: ( dom p) = ( dom x1) by A77, FINSEQ_1:def 3;

              for k be Nat st k in ( dom p) holds (p . k) = (x1 . k)

              proof

                let k be Nat;

                assume

                 A80: k in ( dom p);

                then

                consider r be FinSequence of REAL such that

                 A81: ( dom r) = ( Seg m) and

                 A82: (p . k) = ( Sum r) and

                 A83: for j be Nat st j in ( dom r) holds (r . j) = (a . [k, j]) by A78;

                ex F11 be Finite_Sep_Sequence of S st ( union ( rng F11)) = (F1 . k) & ( dom F11) = ( dom r) & for j be Nat st j in ( dom r) holds (F11 . j) = ((F1 . k) /\ (F2 . j))

                proof

                  deffunc G( set) = ((F1 . k) /\ (F2 . $1));

                  consider F be FinSequence such that

                   A84: ( len F) = m and

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

                  

                   A86: ( dom F) = ( Seg m) by A84, FINSEQ_1:def 3;

                  

                   A87: for i be Nat st i in ( dom F) holds (F . i) in S

                  proof

                    let i be Nat;

                    assume

                     A88: i in ( dom F);

                    then i in ( Seg m) by A84, FINSEQ_1:def 3;

                    then i in ( dom F2) by A13, FINSEQ_1:def 3;

                    then

                     A89: (F2 . i) in ( rng F2) by FUNCT_1: 3;

                    (F1 . k) in ( rng F1) by A27, A79, A80, FUNCT_1: 3;

                    then ((F1 . k) /\ (F2 . i)) in S by A89, MEASURE1: 34;

                    hence thesis by A85, A88;

                  end;

                  

                   A90: ( dom F) = ( Seg m) by A84, FINSEQ_1:def 3;

                  reconsider F as FinSequence of S by A87, FINSEQ_2: 12;

                  

                   A91: ( dom F) = ( dom F2) by A13, A90, FINSEQ_1:def 3;

                  then

                  reconsider F as Finite_Sep_Sequence of S by A85, Th5;

                  take F;

                  ( union ( rng F)) = ((F1 . k) /\ ( union ( rng F2))) by A85, A91, Th6

                  .= ((F1 . k) /\ ( dom f)) by A10

                  .= ((F1 . k) /\ ( union ( rng F1))) by A24

                  .= (F1 . k) by A27, A79, A80, Th7;

                  hence thesis by A81, A85, A86;

                end;

                then

                consider F11 be Finite_Sep_Sequence of S such that

                 A92: ( union ( rng F11)) = (F1 . k) and

                 A93: ( dom F11) = ( dom r) and

                 A94: for j be Nat st j in ( dom r) holds (F11 . j) = ((F1 . k) /\ (F2 . j));

                

                 A95: ( Sum (M * F11)) = (M . (F1 . k)) by A92, Th9;

                k in ( Seg ( len a1)) by A27, A30, A79, A80, FINSEQ_1:def 3;

                then

                 A96: 1 <= k by FINSEQ_1: 1;

                (a1 . k) <> -infty & (a1 . k) <> +infty

                proof

                  per cases ;

                    suppose k = 1;

                    hence thesis by A25;

                  end;

                    suppose k <> 1;

                    then 1 < k by A96, XXREAL_0: 1;

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

                    hence thesis by A26, A27, A30, A79, A80;

                  end;

                end;

                then

                 A97: (a1 . k) is Element of REAL by XXREAL_0: 14;

                reconsider rr = r as FinSequence of ExtREAL by Th11;

                

                 A98: for j be Nat st j in ( dom r) holds (r . j) = ((a1 . k) * (M . ((F1 . k) /\ (F2 . j))))

                proof

                  let j be Nat;

                  assume

                   A99: j in ( dom r);

                  

                  hence (r . j) = (a . (k,j)) by A83

                  .= ((a1 . k) * (M . ((F1 . k) /\ (F2 . j)))) by A70, A77, A80, A81, A99;

                end;

                

                 A100: for j be Nat st j in ( dom rr) holds (rr . j) = ((a1 . k) * ((M * F11) . j))

                proof

                  let j be Nat;

                  assume

                   A101: j in ( dom rr);

                  

                  hence (rr . j) = ((a1 . k) * (M . ((F1 . k) /\ (F2 . j)))) by A98

                  .= ((a1 . k) * (M . (F11 . j))) by A94, A101

                  .= ((a1 . k) * ((M * F11) . j)) by A93, A101, FUNCT_1: 13;

                end;

                ( dom rr) = ( dom (M * F11)) by A93, Th8;

                then ( Sum rr) = ((a1 . k) * ( Sum (M * F11))) by A100, A97, Th10;

                

                then ( Sum r) = ((a1 . k) * (M . (F1 . k))) by A95, Th2

                .= ((a1 . k) * ((M * F1) . k)) by A27, A79, A80, FUNCT_1: 13;

                hence thesis by A28, A79, A80, A82;

              end;

              then

               A102: ( Sum p) = ( Sum x1) by A79, Th2, FINSEQ_1: 13;

              ex q be FinSequence of REAL st ( dom q) = ( Seg m) & for j be Nat st j in ( dom q) holds ex s be FinSequence of REAL st (( dom s) = ( Seg n) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . [i, j]))

              proof

                defpred P[ Nat, object] means ex s be FinSequence of REAL st ( dom s) = ( Seg n) & $2 = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . [i, $1]);

                

                 A103: for k be Nat st k in ( Seg m) holds ex x be object st P[k, x]

                proof

                  let k be Nat;

                  assume k in ( Seg m);

                  deffunc G( set) = (a . [$1, k]);

                  consider s be FinSequence such that

                   A104: ( len s) = n and

                   A105: for i be Nat st i in ( dom s) holds (s . i) = G(i) from FINSEQ_1:sch 2;

                  

                   A106: ( dom s) = ( Seg n) by A104, FINSEQ_1:def 3;

                  for i be Nat st i in ( dom s) holds (s . i) in REAL

                  proof

                    let i be Nat;

                    

                     A107: (a . [i, k]) in REAL by XREAL_0:def 1;

                    assume i in ( dom s);

                    hence thesis by A105, A107;

                  end;

                  then

                  reconsider s as FinSequence of REAL by FINSEQ_2: 12;

                  take x = ( Sum s);

                  thus thesis by A105, A106;

                end;

                consider p be FinSequence such that

                 A108: ( dom p) = ( Seg m) & for k be Nat st k in ( Seg m) holds P[k, (p . k)] from FINSEQ_1:sch 1( A103);

                for i be Nat st i in ( dom p) holds (p . i) in REAL

                proof

                  let i be Nat;

                  assume i in ( dom p);

                  then ex s be FinSequence of REAL st ( dom s) = ( Seg n) & (p . i) = ( Sum s) & for j be Nat st j in ( dom s) holds (s . j) = (a . [j, i]) by A108;

                  hence thesis by XREAL_0:def 1;

                end;

                then

                reconsider p as FinSequence of REAL by FINSEQ_2: 12;

                take p;

                thus thesis by A108;

              end;

              then

              consider q be FinSequence of REAL such that

               A109: ( dom q) = ( Seg m) and

               A110: for j be Nat st j in ( dom q) holds ex s be FinSequence of REAL st (( dom s) = ( Seg n) & (q . j) = ( Sum s) & for i be Nat st i in ( dom s) holds (s . i) = (a . [i, j]));

              

               A111: ( dom q) = ( dom x2) by A109, FINSEQ_1:def 3;

              

               A112: for k be Nat st k in ( dom q) holds (q . k) = (x2 . k)

              proof

                let k be Nat;

                assume

                 A113: k in ( dom q);

                then

                consider s be FinSequence of REAL such that

                 A114: ( dom s) = ( Seg n) and

                 A115: (q . k) = ( Sum s) and

                 A116: for i be Nat st i in ( dom s) holds (s . i) = (a . [i, k]) by A110;

                reconsider ss = s as FinSequence of ExtREAL by Th11;

                ex F21 be Finite_Sep_Sequence of S st ( union ( rng F21)) = (F2 . k) & ( dom F21) = ( dom s) & for j be Nat st j in ( dom s) holds (F21 . j) = ((F1 . j) /\ (F2 . k))

                proof

                  deffunc G( set) = ((F2 . k) /\ (F1 . $1));

                  consider F be FinSequence such that

                   A117: ( len F) = n and

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

                  

                   A119: ( dom F) = ( Seg n) by A117, FINSEQ_1:def 3;

                  

                   A120: for i be Nat st i in ( dom F) holds (F . i) in S

                  proof

                    let i be Nat;

                    assume

                     A121: i in ( dom F);

                    then i in ( Seg n) by A117, FINSEQ_1:def 3;

                    then i in ( dom F1) by A27, FINSEQ_1:def 3;

                    then

                     A122: (F1 . i) in ( rng F1) by FUNCT_1: 3;

                    (F2 . k) in ( rng F2) by A13, A111, A113, FUNCT_1: 3;

                    then ((F1 . i) /\ (F2 . k)) in S by A122, MEASURE1: 34;

                    hence thesis by A118, A121;

                  end;

                  

                   A123: ( dom F) = ( Seg n) by A117, FINSEQ_1:def 3;

                  reconsider F as FinSequence of S by A120, FINSEQ_2: 12;

                  

                   A124: ( dom F) = ( dom F1) by A27, A123, FINSEQ_1:def 3;

                  then

                  reconsider F as Finite_Sep_Sequence of S by A118, Th5;

                  take F;

                  ( union ( rng F)) = ((F2 . k) /\ ( union ( rng F1))) by A118, A124, Th6

                  .= ((F2 . k) /\ ( dom f)) by A24

                  .= ((F2 . k) /\ ( union ( rng F2))) by A10

                  .= (F2 . k) by A13, A111, A113, Th7;

                  hence thesis by A114, A118, A119;

                end;

                then

                consider F21 be Finite_Sep_Sequence of S such that

                 A125: ( union ( rng F21)) = (F2 . k) and

                 A126: ( dom F21) = ( dom s) and

                 A127: for i be Nat st i in ( dom s) holds (F21 . i) = ((F1 . i) /\ (F2 . k));

                

                 A128: ( Sum (M * F21)) = (M . (F2 . k)) by A125, Th9;

                

                 A129: for i be Nat st i in ( dom s) holds (s . i) = ((a1 . i) * (M . ((F1 . i) /\ (F2 . k))))

                proof

                  let i be Nat;

                  assume

                   A130: i in ( dom s);

                  

                  hence (s . i) = (a . (i,k)) by A116

                  .= ((a1 . i) * (M . ((F1 . i) /\ (F2 . k)))) by A70, A109, A113, A114, A130;

                end;

                

                 A131: for i be Nat st i in ( dom s) holds (s . i) = ((a2 . k) * (M . ((F1 . i) /\ (F2 . k))))

                proof

                  let i be Nat;

                  assume

                   A132: i in ( dom s);

                  now

                    per cases ;

                      case

                       A133: ((F1 . i) /\ (F2 . k)) = {} ;

                      then (M . ((F1 . i) /\ (F2 . k))) = 0. by VALUED_0:def 19;

                      

                      hence (s . i) = ((a1 . i) * 0. ) by A129, A132

                      .= 0.

                      .= ((a2 . k) * 0. )

                      .= ((a2 . k) * (M . ((F1 . i) /\ (F2 . k)))) by A133, VALUED_0:def 19;

                    end;

                      case ((F1 . i) /\ (F2 . k)) <> {} ;

                      then

                      consider x be object such that

                       A134: x in ((F1 . i) /\ (F2 . k)) by XBOOLE_0:def 1;

                      

                       A135: x in (F2 . k) by A134, XBOOLE_0:def 4;

                      

                       A136: ( dom p) = ( dom x1) by A77, FINSEQ_1:def 3;

                      x in (F1 . i) by A134, XBOOLE_0:def 4;

                      

                      then (a1 . i) = (f . x) by A24, A27, A77, A114, A132, A136

                      .= (a2 . k) by A10, A13, A111, A113, A135;

                      hence thesis by A129, A132;

                    end;

                  end;

                  hence thesis;

                end;

                

                 A137: for j be Nat st j in ( dom ss) holds (ss . j) = ((a2 . k) * ((M * F21) . j))

                proof

                  let j be Nat;

                  assume

                   A138: j in ( dom ss);

                  

                  hence (ss . j) = ((a2 . k) * (M . ((F1 . j) /\ (F2 . k)))) by A131

                  .= ((a2 . k) * (M . (F21 . j))) by A127, A138

                  .= ((a2 . k) * ((M * F21) . j)) by A126, A138, FUNCT_1: 13;

                end;

                k in ( Seg ( len a2)) by A13, A16, A111, A113, FINSEQ_1:def 3;

                then

                 A139: 1 <= k by FINSEQ_1: 1;

                (a2 . k) <> -infty & (a2 . k) <> +infty

                proof

                  per cases ;

                    suppose k = 1;

                    hence thesis by A11;

                  end;

                    suppose k <> 1;

                    then 1 < k by A139, XXREAL_0: 1;

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

                    hence thesis by A12, A13, A16, A111, A113;

                  end;

                end;

                then

                 A140: (a2 . k) is Element of REAL by XXREAL_0: 14;

                ( dom ss) = ( dom (M * F21)) by A126, Th8;

                then ( Sum ss) = ((a2 . k) * ( Sum (M * F21))) by A137, A140, Th10;

                

                then ( Sum s) = ((a2 . k) * (M . (F2 . k))) by A128, Th2

                .= ((a2 . k) * ((M * F2) . k)) by A13, A111, A113, FUNCT_1: 13;

                hence thesis by A14, A111, A113, A115;

              end;

              ( Sum p) = ( Sum q) by A77, A78, A109, A110, Th1;

              hence thesis by A29, A15, A102, A111, A112, Th2, FINSEQ_1: 13;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    begin

    theorem :: MESFUNC3:18

    for a be FinSequence of ExtREAL , p,N be Element of ExtREAL st N = ( len a) & (for n be Nat st n in ( dom a) holds (a . n) = p) holds ( Sum a) = (N * p) by Lm1;