mesfunc8.miz



    begin

    reserve n,k for Nat,

X for non empty set,

S for SigmaField of X;

    theorem :: MESFUNC8:1

    

     Th1: for M be sigma_Measure of S, F be sequence of S, n holds { x where x be Element of X : for k st n <= k holds x in (F . k) } is Element of S

    proof

      let M be sigma_Measure of S, F be sequence of S, n;

      set G = { x where x be Element of X : for k st n <= k holds x in (F . k) };

      deffunc Fn( Element of NAT ) = (F . (n + $1));

      consider E be sequence of S such that

       A1: for k be Element of NAT holds (E . k) = Fn(k) from FUNCT_2:sch 4;

      now

        let z be object;

        assume z in G;

        then

         A2: ex x be Element of X st z = x & for k be Nat st n <= k holds x in (F . k);

        for Y be set st Y in ( rng E) holds z in Y

        proof

          let Y be set;

          assume Y in ( rng E);

          then

          consider l be object such that

           A3: l in NAT and

           A4: Y = (E . l) by FUNCT_2: 11;

          reconsider l as Element of NAT by A3;

          z in (F . (n + l)) by A2, NAT_1: 12;

          hence thesis by A1, A4;

        end;

        hence z in ( meet ( rng E)) by SETFAM_1:def 1;

      end;

      then

       A5: G c= ( meet ( rng E));

      ( rng E) is N_Sub_set_fam of X by MEASURE1: 23;

      then ( rng E) is N_Measure_fam of S by MEASURE2:def 1;

      then

       A6: ( meet ( rng E)) is Element of S by MEASURE2: 2;

      now

        let z be object;

        assume

         A7: z in ( meet ( rng E));

        now

          let k be Nat;

          assume n <= k;

          then

          reconsider l = (k - n) as Element of NAT by NAT_1: 21;

          (E . l) in ( rng E) by FUNCT_2: 4;

          then z in (E . l) by A7, SETFAM_1:def 1;

          then z in (F . (n + l)) by A1;

          hence z in (F . k);

        end;

        hence z in G by A6, A7;

      end;

      then ( meet ( rng E)) c= G;

      hence thesis by A6, A5, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC8:2

    

     Th2: for F be SetSequence of X, n be Nat holds (( superior_setsequence F) . n) = ( union ( rng (F ^\ n))) & (( inferior_setsequence F) . n) = ( meet ( rng (F ^\ n)))

    proof

      let F be SetSequence of X, n be Nat;

      { (F . k) where k be Nat : n <= k } = ( rng (F ^\ n)) by SETLIM_1: 6;

      hence (( superior_setsequence F) . n) = ( union ( rng (F ^\ n))) by SETLIM_1:def 3;

      (( inferior_setsequence F) . n) = ( meet { (F . k) where k : n <= k }) by SETLIM_1:def 2;

      hence thesis by SETLIM_1: 6;

    end;

    theorem :: MESFUNC8:3

    

     Th3: for M be sigma_Measure of S, F be SetSequence of S holds ex G be sequence of S st G = ( inferior_setsequence F) & (M . ( lim_inf F)) = ( sup ( rng (M * G)))

    proof

      let M be sigma_Measure of S, F be SetSequence of S;

      ( rng ( inferior_setsequence F)) c= S;

      then

      reconsider G = ( inferior_setsequence F) as sequence of S by FUNCT_2: 6;

      for n be Nat holds (G . n) c= (G . (n + 1)) by PROB_1:def 5, NAT_1: 12;

      then (M . ( union ( rng G))) = ( sup ( rng (M * G))) by MEASURE2: 23;

      hence thesis;

    end;

    theorem :: MESFUNC8:4

    

     Th4: for M be sigma_Measure of S, F be SetSequence of S st (M . ( Union F)) < +infty holds ex G be sequence of S st G = ( superior_setsequence F) & (M . ( lim_sup F)) = ( inf ( rng (M * G)))

    proof

      let M be sigma_Measure of S, F be SetSequence of S;

      ( rng ( superior_setsequence F)) c= S;

      then

      reconsider G = ( superior_setsequence F) as sequence of S by FUNCT_2: 6;

      reconsider F1 = F, G1 = G as SetSequence of X;

      

       A1: for n be Nat holds (G . (n + 1)) c= (G . n) by NAT_1: 12, PROB_1:def 4;

      (G . 0 ) = ( union { (F . k) where k : 0 <= k }) by SETLIM_1:def 3;

      then

       A2: (G . 0 ) = ( union ( rng F)) by SETLIM_1: 5;

      consider f be SetSequence of X such that

       A3: ( lim_sup F1) = ( meet f) and

       A4: for n be Nat holds (f . n) = ( Union (F1 ^\ n)) by KURATO_0:def 2;

      now

        let n be Element of NAT ;

        (f . n) = ( Union (F1 ^\ n)) by A4;

        hence (f . n) = (G1 . n) by Th2;

      end;

      then

       A5: f = G1 by FUNCT_2: 63;

      assume (M . ( Union F)) < +infty ;

      then (M . ( meet ( rng G))) = ( inf ( rng (M * G))) by A1, A2, MEASURE3: 12;

      hence thesis by A3, A5;

    end;

    theorem :: MESFUNC8:5

    for M be sigma_Measure of S, F be SetSequence of S st F is convergent holds ex G be sequence of S st G = ( inferior_setsequence F) & (M . ( lim F)) = ( sup ( rng (M * G)))

    proof

      let M be sigma_Measure of S, F be SetSequence of S;

      assume F is convergent;

      then ( lim_inf F) = ( lim F) by KURATO_0:def 5;

      hence thesis by Th3;

    end;

    theorem :: MESFUNC8:6

    for M be sigma_Measure of S, F be SetSequence of S st F is convergent & (M . ( Union F)) < +infty holds ex G be sequence of S st G = ( superior_setsequence F) & (M . ( lim F)) = ( inf ( rng (M * G))) by Th4;

    definition

      let X,Y be set, F be Functional_Sequence of X, Y;

      :: MESFUNC8:def1

      attr F is with_the_same_dom means ( rng F) is with_common_domain;

    end

    definition

      let X,Y be set, F be Functional_Sequence of X, Y;

      :: original: with_the_same_dom

      redefine

      :: MESFUNC8:def2

      attr F is with_the_same_dom means

      : Def2: for n,m be Nat holds ( dom (F . n)) = ( dom (F . m));

      correctness

      proof

        

         A1: (for n,m be Nat holds ( dom (F . n)) = ( dom (F . m))) implies F is with_the_same_dom

        proof

          assume

           A2: for n,m be Nat holds ( dom (F . n)) = ( dom (F . m));

          now

            let f,g be Function;

            assume that

             A3: f in ( rng F) and

             A4: g in ( rng F);

            consider m be object such that

             A5: m in ( dom F) and

             A6: g = (F . m) by A4, FUNCT_1:def 3;

            consider n be object such that

             A7: n in ( dom F) and

             A8: f = (F . n) by A3, FUNCT_1:def 3;

            reconsider n, m as Nat by A7, A5;

            ( dom (F . n)) = ( dom (F . m)) by A2;

            hence ( dom f) = ( dom g) by A8, A6;

          end;

          then ( rng F) is with_common_domain;

          hence thesis;

        end;

        F is with_the_same_dom implies for n,m be Nat holds ( dom (F . n)) = ( dom (F . m))

        proof

          assume F is with_the_same_dom;

          then

           A9: ( rng F) is with_common_domain;

          hereby

            let n,m be Nat;

            

             A10: ( dom F) = NAT by FUNCT_2:def 1;

            then m in ( dom F) by ORDINAL1:def 12;

            then

             A11: (F . m) in ( rng F) by FUNCT_1: 3;

            n in ( dom F) by A10, ORDINAL1:def 12;

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

            hence ( dom (F . n)) = ( dom (F . m)) by A9, A11;

          end;

        end;

        hence thesis by A1;

      end;

    end

    registration

      let X,Y be set;

      cluster with_the_same_dom for Functional_Sequence of X, Y;

      existence

      proof

        deffunc f( Nat) = <: {} , X, Y:>;

        consider F be Functional_Sequence of X, Y such that

         A1: for n be Nat holds (F . n) = f(n) from SEQFUNC:sch 1;

        take F;

        hereby

          let n,m be Nat;

          (F . n) = <: {} , X, Y:> by A1;

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

        end;

      end;

    end

    definition

      let X be non empty set, f be Functional_Sequence of X, ExtREAL ;

      :: MESFUNC8:def3

      func inf f -> PartFunc of X, ExtREAL means

      : Def3: ( dom it ) = ( dom (f . 0 )) & for x be Element of X st x in ( dom it ) holds (it . x) = ( inf (f # x));

      existence

      proof

        defpred P[ set] means $1 in ( dom (f . 0 ));

        deffunc F( Element of X) = ( inf (f # $1));

        consider g be PartFunc of X, ExtREAL such that

         A1: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

        take g;

         A2:

        now

          let x be Element of X;

          assume

           A3: x in ( dom g);

          then (g /. x) = ( inf (f # x)) by A1;

          hence (g . x) = ( inf (f # x)) by A3, PARTFUN1:def 6;

        end;

        for x be object holds x in ( dom g) iff x in ( dom (f . 0 )) by A1;

        hence thesis by A2, TARSKI: 2;

      end;

      uniqueness

      proof

        let g,h be PartFunc of X, ExtREAL ;

        assume that

         A4: ( dom g) = ( dom (f . 0 )) and

         A5: for x be Element of X st x in ( dom g) holds (g . x) = ( inf (f # x));

        assume that

         A6: ( dom h) = ( dom (f . 0 )) and

         A7: for x be Element of X st x in ( dom h) holds (h . x) = ( inf (f # x));

        now

          let x be Element of X;

          assume

           A8: x in ( dom g);

          then (g /. x) = (g . x) by PARTFUN1:def 6;

          then (g /. x) = ( inf (f # x)) by A5, A8;

          then (g /. x) = (h . x) by A4, A6, A7, A8;

          hence (g /. x) = (h /. x) by A4, A6, A8, PARTFUN1:def 6;

        end;

        hence thesis by A4, A6, PARTFUN2: 1;

      end;

    end

    definition

      let X be non empty set, f be Functional_Sequence of X, ExtREAL ;

      :: MESFUNC8:def4

      func sup f -> PartFunc of X, ExtREAL means

      : Def4: ( dom it ) = ( dom (f . 0 )) & for x be Element of X st x in ( dom it ) holds (it . x) = ( sup (f # x));

      existence

      proof

        defpred P[ set] means $1 in ( dom (f . 0 ));

        deffunc F( Element of X) = ( sup (f # $1));

        consider g be PartFunc of X, ExtREAL such that

         A1: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

        take g;

         A2:

        now

          let x be Element of X;

          assume

           A3: x in ( dom g);

          then (g /. x) = ( sup (f # x)) by A1;

          hence (g . x) = ( sup (f # x)) by A3, PARTFUN1:def 6;

        end;

        for x be object holds x in ( dom g) iff x in ( dom (f . 0 )) by A1;

        hence thesis by A2, TARSKI: 2;

      end;

      uniqueness

      proof

        let g,h be PartFunc of X, ExtREAL ;

        assume that

         A4: ( dom g) = ( dom (f . 0 )) and

         A5: for x be Element of X st x in ( dom g) holds (g . x) = ( sup (f # x));

        assume that

         A6: ( dom h) = ( dom (f . 0 )) and

         A7: for x be Element of X st x in ( dom h) holds (h . x) = ( sup (f # x));

        now

          let x be Element of X;

          assume

           A8: x in ( dom g);

          then (g /. x) = (g . x) by PARTFUN1:def 6;

          then (g /. x) = ( sup (f # x)) by A5, A8;

          then (g /. x) = (h . x) by A4, A6, A7, A8;

          hence (g /. x) = (h /. x) by A4, A6, A8, PARTFUN1:def 6;

        end;

        hence thesis by A4, A6, PARTFUN2: 1;

      end;

    end

    definition

      let X be non empty set, f be Functional_Sequence of X, ExtREAL ;

      :: MESFUNC8:def5

      func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X, ExtREAL means

      : Def5: for n be Nat holds ( dom (it . n)) = ( dom (f . 0 )) & for x be Element of X st x in ( dom (it . n)) holds ((it . n) . x) = (( inferior_realsequence (f # x)) . n);

      existence

      proof

        defpred P[ Element of NAT , Function] means ( dom $2) = ( dom (f . 0 )) & for x be Element of X st x in ( dom $2) holds ($2 . x) = (( inferior_realsequence (f # x)) . $1);

        

         A1: for n be Element of NAT holds ex y be Element of ( PFuncs (X, ExtREAL )) st P[n, y]

        proof

          defpred P[ set] means $1 in ( dom (f . 0 ));

          let n be Element of NAT ;

          deffunc F( Element of X) = (( inferior_realsequence (f # $1)) . n);

          consider g be PartFunc of X, ExtREAL such that

           A2: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

          take g;

           A3:

          now

            let x be Element of X;

            assume

             A4: x in ( dom g);

            then (g /. x) = (( inferior_realsequence (f # x)) . n) by A2;

            hence (g . x) = (( inferior_realsequence (f # x)) . n) by A4, PARTFUN1:def 6;

          end;

          for x be object holds x in ( dom g) iff x in ( dom (f . 0 )) by A2;

          hence thesis by A3, PARTFUN1: 45, TARSKI: 2;

        end;

        consider g be sequence of ( PFuncs (X, ExtREAL )) such that

         A5: for n be Element of NAT holds P[n, (g . n)] from FUNCT_2:sch 3( A1);

        

         A6: for n holds ( dom (g . n)) = ( dom (f . 0 )) & for x be Element of X st x in ( dom (g . n)) holds ((g . n) . x) = (( inferior_realsequence (f # x)) . n)

        proof

          let n;

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

          ( dom (g . n9)) = ( dom (f . 0 )) by A5;

          hence thesis by A5;

        end;

        reconsider g as Functional_Sequence of X, ExtREAL ;

        now

          let k,l be Nat;

          reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def 12;

          ( dom (g . k9)) = ( dom (f . 0 )) by A5;

          then ( dom (g . k)) = ( dom (g . l9)) by A5;

          hence ( dom (g . k)) = ( dom (g . l));

        end;

        then

        reconsider g as with_the_same_dom Functional_Sequence of X, ExtREAL by Def2;

        take g;

        thus thesis by A6;

      end;

      uniqueness

      proof

        let g,h be with_the_same_dom Functional_Sequence of X, ExtREAL ;

        assume

         A7: for n be Nat holds ( dom (g . n)) = ( dom (f . 0 )) & for x be Element of X st x in ( dom (g . n)) holds ((g . n) . x) = (( inferior_realsequence (f # x)) . n);

        assume

         A8: for n be Nat holds ( dom (h . n)) = ( dom (f . 0 )) & for x be Element of X st x in ( dom (h . n)) holds ((h . n) . x) = (( inferior_realsequence (f # x)) . n);

        now

          let n be Element of NAT ;

          

           A9: ( dom (g . n)) = ( dom (f . 0 )) by A7

          .= ( dom (h . n)) by A8;

          now

            let x be Element of X;

            assume

             A10: x in ( dom (g . n));

            then ((g . n) /. x) = ((g . n) . x) by PARTFUN1:def 6;

            then ((g . n) /. x) = (( inferior_realsequence (f # x)) . n) by A7, A10;

            then ((g . n) /. x) = ((h . n) . x) by A8, A9, A10;

            hence ((g . n) /. x) = ((h . n) /. x) by A9, A10, PARTFUN1:def 6;

          end;

          hence (g . n) = (h . n) by A9, PARTFUN2: 1;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let X be non empty set, f be Functional_Sequence of X, ExtREAL ;

      :: MESFUNC8:def6

      func superior_realsequence f -> with_the_same_dom Functional_Sequence of X, ExtREAL means

      : Def6: for n be Nat holds ( dom (it . n)) = ( dom (f . 0 )) & for x be Element of X st x in ( dom (it . n)) holds ((it . n) . x) = (( superior_realsequence (f # x)) . n);

      existence

      proof

        defpred P[ Element of NAT , Function] means ( dom $2) = ( dom (f . 0 )) & for x be Element of X st x in ( dom $2) holds ($2 . x) = (( superior_realsequence (f # x)) . $1);

        

         A1: for n be Element of NAT holds ex y be Element of ( PFuncs (X, ExtREAL )) st P[n, y]

        proof

          defpred P[ set] means $1 in ( dom (f . 0 ));

          let n be Element of NAT ;

          deffunc F( Element of X) = (( superior_realsequence (f # $1)) . n);

          consider g be PartFunc of X, ExtREAL such that

           A2: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

          take g;

           A3:

          now

            let x be Element of X;

            assume

             A4: x in ( dom g);

            then (g /. x) = (( superior_realsequence (f # x)) . n) by A2;

            hence (g . x) = (( superior_realsequence (f # x)) . n) by A4, PARTFUN1:def 6;

          end;

          for x be object holds x in ( dom g) iff x in ( dom (f . 0 )) by A2;

          hence thesis by A3, PARTFUN1: 45, TARSKI: 2;

        end;

        consider g be sequence of ( PFuncs (X, ExtREAL )) such that

         A5: for n be Element of NAT holds P[n, (g . n)] from FUNCT_2:sch 3( A1);

        

         A6: for n holds ( dom (g . n)) = ( dom (f . 0 )) & for x be Element of X st x in ( dom (g . n)) holds ((g . n) . x) = (( superior_realsequence (f # x)) . n)

        proof

          let n;

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

          ( dom (g . n9)) = ( dom (f . 0 )) by A5;

          hence thesis by A5;

        end;

        reconsider g as Functional_Sequence of X, ExtREAL ;

        now

          let k,l be Nat;

          reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def 12;

          ( dom (g . k9)) = ( dom (f . 0 )) by A5;

          then ( dom (g . k)) = ( dom (g . l9)) by A5;

          hence ( dom (g . k)) = ( dom (g . l));

        end;

        then

        reconsider g as with_the_same_dom Functional_Sequence of X, ExtREAL by Def2;

        take g;

        thus thesis by A6;

      end;

      uniqueness

      proof

        let g,h be with_the_same_dom Functional_Sequence of X, ExtREAL ;

        assume

         A7: for n holds ( dom (g . n)) = ( dom (f . 0 )) & for x be Element of X st x in ( dom (g . n)) holds ((g . n) . x) = (( superior_realsequence (f # x)) . n);

        assume

         A8: for n holds ( dom (h . n)) = ( dom (f . 0 )) & for x be Element of X st x in ( dom (h . n)) holds ((h . n) . x) = (( superior_realsequence (f # x)) . n);

        now

          let n be Element of NAT ;

          

           A9: ( dom (g . n)) = ( dom (f . 0 )) by A7

          .= ( dom (h . n)) by A8;

          now

            let x be Element of X;

            assume

             A10: x in ( dom (g . n));

            then ((g . n) /. x) = ((g . n) . x) by PARTFUN1:def 6;

            then ((g . n) /. x) = (( superior_realsequence (f # x)) . n) by A7, A10;

            then ((g . n) /. x) = ((h . n) . x) by A8, A9, A10;

            hence ((g . n) /. x) = ((h . n) /. x) by A9, A10, PARTFUN1:def 6;

          end;

          hence (g . n) = (h . n) by A9, PARTFUN2: 1;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: MESFUNC8:7

    

     Th7: for f be Functional_Sequence of X, ExtREAL holds for x be Element of X st x in ( dom (f . 0 )) holds (( inferior_realsequence f) # x) = ( inferior_realsequence (f # x))

    proof

      let f be Functional_Sequence of X, ExtREAL ;

      set F = ( inferior_realsequence f);

      hereby

        let x be Element of X;

        assume

         A1: x in ( dom (f . 0 ));

        now

          let n be Element of NAT ;

          

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

          ( dom (F . n)) = ( dom (f . 0 )) by Def5;

          hence ((F # x) . n) = (( inferior_realsequence (f # x)) . n) by A1, A2, Def5;

        end;

        hence (F # x) = ( inferior_realsequence (f # x)) by FUNCT_2: 63;

      end;

    end;

    registration

      let X,Y be set;

      let f be with_the_same_dom Functional_Sequence of X, Y;

      let n be Nat;

      cluster (f ^\ n) -> with_the_same_dom;

      coherence

      proof

        for k,l be Nat holds ( dom ((f ^\ n) . k)) = ( dom ((f ^\ n) . l))

        proof

          reconsider g = f as sequence of ( PFuncs (X,Y));

          let k,l be Nat;

          reconsider k9 = k, l9 = l as Element of NAT by ORDINAL1:def 12;

          ( dom ((f ^\ n) . k)) = ( dom (g . (n + k9))) by NAT_1:def 3;

          then ( dom ((f ^\ n) . k)) = ( dom (g . (n + l9))) by Def2;

          hence thesis by NAT_1:def 3;

        end;

        hence thesis;

      end;

    end

    theorem :: MESFUNC8:8

    

     Th8: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , n be Nat holds (( inferior_realsequence f) . n) = ( inf (f ^\ n))

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , n be Nat;

      reconsider g = f as sequence of ( PFuncs (X, ExtREAL ));

      ( dom ( inf (f ^\ n))) = ( dom ((f ^\ n) . 0 )) by Def3;

      then ( dom ( inf (f ^\ n))) = ( dom (g . (n + 0 qua Nat))) by NAT_1:def 3;

      then

       A1: ( dom ( inf (f ^\ n))) = ( dom (f . 0 )) by Def2;

      

       A2: ( dom (( inferior_realsequence f) . n)) = ( dom (f . 0 )) by Def5;

      now

        let x be Element of X;

        assume

         A3: x in ( dom ( inf (f ^\ n)));

        now

          let k be Element of NAT ;

          (((f ^\ n) # x) . k) = (((f ^\ n) . k) . x) by MESFUNC5:def 13;

          then (((f ^\ n) # x) . k) = ((g . (n + k)) . x) by NAT_1:def 3;

          then (((f ^\ n) # x) . k) = ((f # x) . (n + k)) by MESFUNC5:def 13;

          hence (((f ^\ n) # x) . k) = (((f # x) ^\ n) . k) by NAT_1:def 3;

        end;

        then ((f ^\ n) # x) = ((f # x) ^\ n) by FUNCT_2: 63;

        then

         A4: (( inf (f ^\ n)) . x) = ( inf ((f # x) ^\ n)) by A3, Def3;

        ((( inferior_realsequence f) . n) . x) = (( inferior_realsequence (f # x)) . n) by A2, A1, A3, Def5;

        hence (( inf (f ^\ n)) . x) = ((( inferior_realsequence f) . n) . x) by A4, RINFSUP2: 27;

      end;

      hence thesis by A2, A1, PARTFUN1: 5;

    end;

    theorem :: MESFUNC8:9

    

     Th9: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , n be Nat holds (( superior_realsequence f) . n) = ( sup (f ^\ n))

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , n be Nat;

      reconsider g = f as sequence of ( PFuncs (X, ExtREAL ));

      ( dom ( sup (f ^\ n))) = ( dom ((f ^\ n) . 0 )) by Def4;

      then ( dom ( sup (f ^\ n))) = ( dom (g . (n + 0 qua Nat))) by NAT_1:def 3;

      then

       A1: ( dom ( sup (f ^\ n))) = ( dom (f . 0 )) by Def2;

      

       A2: ( dom (( superior_realsequence f) . n)) = ( dom (f . 0 )) by Def6;

      now

        let x be Element of X;

        assume

         A3: x in ( dom ( sup (f ^\ n)));

        now

          let k be Element of NAT ;

          (((f ^\ n) # x) . k) = (((f ^\ n) . k) . x) by MESFUNC5:def 13;

          then (((f ^\ n) # x) . k) = ((g . (n + k)) . x) by NAT_1:def 3;

          then (((f ^\ n) # x) . k) = ((f # x) . (n + k)) by MESFUNC5:def 13;

          hence (((f ^\ n) # x) . k) = (((f # x) ^\ n) . k) by NAT_1:def 3;

        end;

        then ((f ^\ n) # x) = ((f # x) ^\ n) by FUNCT_2: 63;

        then

         A4: (( sup (f ^\ n)) . x) = ( sup ((f # x) ^\ n)) by A3, Def4;

        ((( superior_realsequence f) . n) . x) = (( superior_realsequence (f # x)) . n) by A2, A1, A3, Def6;

        hence (( sup (f ^\ n)) . x) = ((( superior_realsequence f) . n) . x) by A4, RINFSUP2: 27;

      end;

      hence thesis by A2, A1, PARTFUN1: 5;

    end;

    theorem :: MESFUNC8:10

    

     Th10: for f be Functional_Sequence of X, ExtREAL , x be Element of X st x in ( dom (f . 0 )) holds (( superior_realsequence f) # x) = ( superior_realsequence (f # x))

    proof

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

      set F = ( superior_realsequence f);

      assume

       A1: x in ( dom (f . 0 ));

      now

        let n be Element of NAT ;

        

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

        ( dom (F . n)) = ( dom (f . 0 )) by Def6;

        hence ((F # x) . n) = (( superior_realsequence (f # x)) . n) by A1, A2, Def6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let X be non empty set, f be Functional_Sequence of X, ExtREAL ;

      :: MESFUNC8:def7

      func lim_inf f -> PartFunc of X, ExtREAL means

      : Def7: ( dom it ) = ( dom (f . 0 )) & for x be Element of X st x in ( dom it ) holds (it . x) = ( lim_inf (f # x));

      existence

      proof

        defpred P[ set] means $1 in ( dom (f . 0 ));

        deffunc F( Element of X) = ( lim_inf (f # $1));

        consider g be PartFunc of X, ExtREAL such that

         A1: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

        take g;

         A2:

        now

          let x be Element of X;

          assume

           A3: x in ( dom g);

          then (g /. x) = ( lim_inf (f # x)) by A1;

          hence (g . x) = ( lim_inf (f # x)) by A3, PARTFUN1:def 6;

        end;

        for x be object holds x in ( dom g) iff x in ( dom (f . 0 )) by A1;

        hence thesis by A2, TARSKI: 2;

      end;

      uniqueness

      proof

        let g,h be PartFunc of X, ExtREAL ;

        assume that

         A4: ( dom g) = ( dom (f . 0 )) and

         A5: for x be Element of X st x in ( dom g) holds (g . x) = ( lim_inf (f # x)) and

         A6: ( dom h) = ( dom (f . 0 )) and

         A7: for x be Element of X st x in ( dom h) holds (h . x) = ( lim_inf (f # x));

        now

          let x be Element of X;

          assume

           A8: x in ( dom g);

          then (g /. x) = (g . x) by PARTFUN1:def 6;

          then (g /. x) = ( lim_inf (f # x)) by A5, A8;

          then (g /. x) = (h . x) by A4, A6, A7, A8;

          hence (g /. x) = (h /. x) by A4, A6, A8, PARTFUN1:def 6;

        end;

        hence thesis by A4, A6, PARTFUN2: 1;

      end;

    end

    definition

      let X be non empty set, f be Functional_Sequence of X, ExtREAL ;

      :: MESFUNC8:def8

      func lim_sup f -> PartFunc of X, ExtREAL means

      : Def8: ( dom it ) = ( dom (f . 0 )) & for x be Element of X st x in ( dom it ) holds (it . x) = ( lim_sup (f # x));

      existence

      proof

        defpred P[ set] means $1 in ( dom (f . 0 ));

        deffunc F( Element of X) = ( lim_sup (f # $1));

        consider g be PartFunc of X, ExtREAL such that

         A1: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

        take g;

         A2:

        now

          let x be Element of X;

          assume

           A3: x in ( dom g);

          then (g /. x) = ( lim_sup (f # x)) by A1;

          hence (g . x) = ( lim_sup (f # x)) by A3, PARTFUN1:def 6;

        end;

        for x be object holds x in ( dom g) iff x in ( dom (f . 0 )) by A1;

        hence thesis by A2, TARSKI: 2;

      end;

      uniqueness

      proof

        let g,h be PartFunc of X, ExtREAL ;

        assume that

         A4: ( dom g) = ( dom (f . 0 )) and

         A5: for x be Element of X st x in ( dom g) holds (g . x) = ( lim_sup (f # x));

        assume that

         A6: ( dom h) = ( dom (f . 0 )) and

         A7: for x be Element of X st x in ( dom h) holds (h . x) = ( lim_sup (f # x));

        now

          let x be Element of X;

          assume

           A8: x in ( dom g);

          then (g /. x) = (g . x) by PARTFUN1:def 6;

          then (g /. x) = ( lim_sup (f # x)) by A5, A8;

          then (g /. x) = (h . x) by A4, A6, A7, A8;

          hence (g /. x) = (h /. x) by A4, A6, A8, PARTFUN1:def 6;

        end;

        hence thesis by A4, A6, PARTFUN2: 1;

      end;

    end

    theorem :: MESFUNC8:11

    

     Th11: for f be Functional_Sequence of X, ExtREAL holds (for x be Element of X st x in ( dom ( lim_inf f)) holds (( lim_inf f) . x) = ( sup ( inferior_realsequence (f # x))) & (( lim_inf f) . x) = ( sup (( inferior_realsequence f) # x)) & (( lim_inf f) . x) = (( sup ( inferior_realsequence f)) . x)) & ( lim_inf f) = ( sup ( inferior_realsequence f))

    proof

      let f be Functional_Sequence of X, ExtREAL ;

      ( dom ( sup ( inferior_realsequence f))) = ( dom (( inferior_realsequence f) . 0 )) by Def4;

      then ( dom ( sup ( inferior_realsequence f))) = ( dom (f . 0 )) by Def5;

      then

       A1: ( dom ( sup ( inferior_realsequence f))) = ( dom ( lim_inf f)) by Def7;

       A2:

      now

        let x be Element of X;

        assume

         A3: x in ( dom ( lim_inf f));

        then

         A4: (( lim_inf f) . x) = ( lim_inf (f # x)) by Def7;

        hence (( lim_inf f) . x) = ( sup ( inferior_realsequence (f # x)));

        ( dom ( lim_inf f)) = ( dom (f . 0 )) by Def7;

        hence (( lim_inf f) . x) = ( sup (( inferior_realsequence f) # x)) by A3, A4, Th7;

        hence (( lim_inf f) . x) = (( sup ( inferior_realsequence f)) . x) by A1, A3, Def4;

      end;

      then for x be Element of X st x in ( dom ( lim_inf f)) holds (( lim_inf f) . x) = (( sup ( inferior_realsequence f)) . x);

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: MESFUNC8:12

    

     Th12: for f be Functional_Sequence of X, ExtREAL holds (for x be Element of X st x in ( dom ( lim_sup f)) holds (( lim_sup f) . x) = ( inf ( superior_realsequence (f # x))) & (( lim_sup f) . x) = ( inf (( superior_realsequence f) # x)) & (( lim_sup f) . x) = (( inf ( superior_realsequence f)) . x)) & ( lim_sup f) = ( inf ( superior_realsequence f))

    proof

      let f be Functional_Sequence of X, ExtREAL ;

      

       A1: ( dom ( inf ( superior_realsequence f))) = ( dom (( superior_realsequence f) . 0 )) by Def3

      .= ( dom (f . 0 )) by Def6

      .= ( dom ( lim_sup f)) by Def8;

       A2:

      now

        let x be Element of X;

        assume

         A3: x in ( dom ( lim_sup f));

        then

         A4: (( lim_sup f) . x) = ( lim_sup (f # x)) by Def8;

        hence (( lim_sup f) . x) = ( inf ( superior_realsequence (f # x)));

        ( dom ( lim_sup f)) = ( dom (f . 0 )) by Def8;

        hence (( lim_sup f) . x) = ( inf (( superior_realsequence f) # x)) by A3, A4, Th10;

        hence (( lim_sup f) . x) = (( inf ( superior_realsequence f)) . x) by A1, A3, Def3;

      end;

      then for x be Element of X st x in ( dom ( lim_sup f)) holds (( lim_sup f) . x) = (( inf ( superior_realsequence f)) . x);

      hence thesis by A1, A2, PARTFUN1: 5;

    end;

    theorem :: MESFUNC8:13

    for f be Functional_Sequence of X, ExtREAL , x be Element of X st x in ( dom (f . 0 )) holds (f # x) is convergent iff (( lim_sup f) . x) = (( lim_inf f) . x)

    proof

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

      assume

       A1: x in ( dom (f . 0 ));

      then x in ( dom ( lim_inf f)) by Def7;

      then

       A2: (( lim_inf f) . x) = ( lim_inf (f # x)) by Def7;

      x in ( dom ( lim_sup f)) by A1, Def8;

      then (( lim_sup f) . x) = ( lim_sup (f # x)) by Def8;

      hence thesis by A2, RINFSUP2: 40;

    end;

    definition

      let X be non empty set, f be Functional_Sequence of X, ExtREAL ;

      :: MESFUNC8:def9

      func lim f -> PartFunc of X, ExtREAL means

      : Def9: ( dom it ) = ( dom (f . 0 )) & for x be Element of X st x in ( dom it ) holds (it . x) = ( lim (f # x));

      existence

      proof

        defpred P[ set] means $1 in ( dom (f . 0 ));

        deffunc F( Element of X) = ( lim (f # $1));

        consider g be PartFunc of X, ExtREAL such that

         A1: (for x be Element of X holds x in ( dom g) iff P[x]) & for x be Element of X st x in ( dom g) holds (g /. x) = F(x) from PARTFUN2:sch 2;

        take g;

         A2:

        now

          let x be Element of X;

          assume

           A3: x in ( dom g);

          then (g /. x) = ( lim (f # x)) by A1;

          hence (g . x) = ( lim (f # x)) by A3, PARTFUN1:def 6;

        end;

        for x be object holds x in ( dom g) iff x in ( dom (f . 0 )) by A1;

        hence thesis by A2, TARSKI: 2;

      end;

      uniqueness

      proof

        let g,h be PartFunc of X, ExtREAL ;

        assume that

         A4: ( dom g) = ( dom (f . 0 )) and

         A5: for x be Element of X st x in ( dom g) holds (g . x) = ( lim (f # x));

        assume that

         A6: ( dom h) = ( dom (f . 0 )) and

         A7: for x be Element of X st x in ( dom h) holds (h . x) = ( lim (f # x));

        now

          let x be Element of X;

          assume

           A8: x in ( dom g);

          then (g /. x) = (g . x) by PARTFUN1:def 6;

          then (g /. x) = ( lim (f # x)) by A5, A8;

          then (g /. x) = (h . x) by A4, A6, A7, A8;

          hence (g /. x) = (h /. x) by A4, A6, A8, PARTFUN1:def 6;

        end;

        hence thesis by A4, A6, PARTFUN2: 1;

      end;

    end

    theorem :: MESFUNC8:14

    

     Th14: for f be Functional_Sequence of X, ExtREAL , x be Element of X st x in ( dom ( lim f)) & (f # x) is convergent holds (( lim f) . x) = (( lim_sup f) . x) & (( lim f) . x) = (( lim_inf f) . x)

    proof

      let f be Functional_Sequence of X, ExtREAL ;

      let x be Element of X;

      assume that

       A1: x in ( dom ( lim f)) and

       A2: (f # x) is convergent;

      

       A3: ( lim (f # x)) = ( lim_inf (f # x)) by A2, RINFSUP2: 41;

      

       A4: x in ( dom (f . 0 )) by A1, Def9;

      then x in ( dom ( lim_sup f)) by Def8;

      then

       A5: (( lim_sup f) . x) = ( lim_sup (f # x)) by Def8;

      x in ( dom ( lim_inf f)) by A4, Def7;

      then

       A6: (( lim_inf f) . x) = ( lim_inf (f # x)) by Def7;

      ( lim (f # x)) = ( lim_sup (f # x)) by A2, RINFSUP2: 41;

      hence thesis by A1, A5, A6, A3, Def9;

    end;

    theorem :: MESFUNC8:15

    

     Th15: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real st (for n be Nat holds (F . n) = (( dom (f . 0 )) /\ ( great_dom ((f . n),r)))) holds ( union ( rng F)) = (( dom (f . 0 )) /\ ( great_dom (( sup f),r)))

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real;

      set E = ( dom (f . 0 ));

      assume

       A1: for n be Nat holds (F . n) = (E /\ ( great_dom ((f . n),r)));

      now

        let x be object;

        assume

         A2: x in (E /\ ( great_dom (( sup f),r)));

        then

        reconsider z = x as Element of X;

        

         A3: x in E by A2, XBOOLE_0:def 4;

        x in ( great_dom (( sup f),r)) by A2, XBOOLE_0:def 4;

        then

         A4: r < (( sup f) . z) by MESFUNC1:def 13;

        ex n be Element of NAT st r < ((f . n) . z)

        proof

          assume

           A5: for n be Element of NAT holds ((f . n) . z) <= r;

          for x be ExtReal st x in ( rng (f # z)) holds x <= r

          proof

            let x be ExtReal;

            assume x in ( rng (f # z));

            then

            consider m be object such that

             A6: m in NAT and

             A7: x = ((f # z) . m) by FUNCT_2: 11;

            reconsider m as Element of NAT by A6;

            x = ((f . m) . z) by A7, MESFUNC5:def 13;

            hence thesis by A5;

          end;

          then r is UpperBound of ( rng (f # z)) by XXREAL_2:def 1;

          then

           A8: ( sup (f # z)) <= r by XXREAL_2:def 3;

          x in ( dom ( sup f)) by A3, Def4;

          hence contradiction by A4, A8, Def4;

        end;

        then

        consider n be Element of NAT such that

         A9: r < ((f . n) . z);

        x in ( dom (f . n)) by A3, Def2;

        then

         A10: x in ( great_dom ((f . n),r)) by A9, MESFUNC1:def 13;

        

         A11: (F . n) in ( rng F) by FUNCT_2: 4;

        

         A12: (F . n) = (E /\ ( great_dom ((f . n),r))) by A1;

        x in E by A2, XBOOLE_0:def 4;

        then x in (F . n) by A10, A12, XBOOLE_0:def 4;

        hence x in ( union ( rng F)) by A11, TARSKI:def 4;

      end;

      then

       A13: (E /\ ( great_dom (( sup f),r))) c= ( union ( rng F));

      now

        let x be object;

        assume x in ( union ( rng F));

        then

        consider y be set such that

         A14: x in y and

         A15: y in ( rng F qua SetSequence of X) by TARSKI:def 4;

        reconsider z = x as Element of X by A14, A15;

        consider n be object such that

         A16: n in ( dom F) and

         A17: y = (F . n) by A15, FUNCT_1:def 3;

        reconsider n as Element of NAT by A16;

        

         A18: (F . n) = (E /\ ( great_dom ((f . n),r))) by A1;

        then x in ( great_dom ((f . n),r)) by A14, A17, XBOOLE_0:def 4;

        then

         A19: r < ((f . n) . z) by MESFUNC1:def 13;

        

         A20: ((f . n) . z) = ((f # z) . n) by MESFUNC5:def 13;

        

         A21: x in E by A14, A17, A18, XBOOLE_0:def 4;

        then

         A22: x in ( dom ( sup f)) by Def4;

        then (( sup f) . z) = ( sup (f # z)) by Def4;

        then ((f . n) . z) <= (( sup f) . z) by A20, RINFSUP2: 23;

        then r < (( sup f) . z) by A19, XXREAL_0: 2;

        then x in ( great_dom (( sup f),r)) by A22, MESFUNC1:def 13;

        hence x in (E /\ ( great_dom (( sup f),r))) by A21, XBOOLE_0:def 4;

      end;

      then ( union ( rng F)) c= (E /\ ( great_dom (( sup f),r)));

      hence thesis by A13, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC8:16

    

     Th16: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real st (for n be Nat holds (F . n) = (( dom (f . 0 )) /\ ( great_eq_dom ((f . n),r)))) holds ( meet ( rng F)) = (( dom (f . 0 )) /\ ( great_eq_dom (( inf f),r)))

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real;

      set E = ( dom (f . 0 ));

      assume

       A1: for n be Nat holds (F . n) = (( dom (f . 0 )) /\ ( great_eq_dom ((f . n),r)));

      now

        let x be object;

        assume

         A2: x in ( meet ( rng F qua SetSequence of X));

        then

        reconsider z = x as Element of X;

        

         A3: (F . 0 ) = (E /\ ( great_eq_dom ((f . 0 ),r))) by A1;

        (F . 0 ) in ( rng F) by FUNCT_2: 4;

        then x in (F . 0 ) by A2, SETFAM_1:def 1;

        then

         A4: x in E by A3, XBOOLE_0:def 4;

        then

         A5: x in ( dom ( inf f)) by Def3;

         A6:

        now

          let n be Element of NAT ;

          (F . n) in ( rng F) by FUNCT_2: 4;

          then

           A7: z in (F . n) by A2, SETFAM_1:def 1;

          (F . n) = (E /\ ( great_eq_dom ((f . n),r))) by A1;

          then x in ( great_eq_dom ((f . n),r)) by A7, XBOOLE_0:def 4;

          then r <= ((f . n) . z) by MESFUNC1:def 14;

          hence r <= ((f # z) . n) by MESFUNC5:def 13;

        end;

        now

          let s be ExtReal;

          assume s in ( rng (f # z));

          then ex k be object st k in NAT & s = ((f # z) . k) by FUNCT_2: 11;

          hence r <= s by A6;

        end;

        then r is LowerBound of ( rng (f # z)) by XXREAL_2:def 2;

        then r <= ( inf (f # z)) by XXREAL_2:def 4;

        then r <= (( inf f) . x) by A5, Def3;

        then x in ( great_eq_dom (( inf f),r)) by A5, MESFUNC1:def 14;

        hence x in (E /\ ( great_eq_dom (( inf f),r))) by A4, XBOOLE_0:def 4;

      end;

      then

       A8: ( meet ( rng F)) c= (E /\ ( great_eq_dom (( inf f),r)));

      now

        let x be object;

        assume

         A9: x in (E /\ ( great_eq_dom (( inf f),r)));

        then

        reconsider z = x as Element of X;

        

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

        x in ( great_eq_dom (( inf f),r)) by A9, XBOOLE_0:def 4;

        then

         A11: r <= (( inf f) . z) by MESFUNC1:def 14;

        now

          let y be set;

          assume y in ( rng F);

          then

          consider n be object such that

           A12: n in NAT and

           A13: y = (F . n) by FUNCT_2: 11;

          reconsider n as Element of NAT by A12;

          

           A14: x in ( dom (f . n)) by A10, Def2;

          x in ( dom ( inf f)) by A10, Def3;

          then

           A15: (( inf f) . z) = ( inf (f # z)) by Def3;

          

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

          ((f . n) . z) = ((f # z) . n) by MESFUNC5:def 13;

          then ( inf (f # z)) <= ((f . n) . z) by RINFSUP2: 23;

          then r <= ((f . n) . z) by A11, A15, XXREAL_0: 2;

          then

           A17: x in ( great_eq_dom ((f . n),r)) by A14, MESFUNC1:def 14;

          (F . n) = (E /\ ( great_eq_dom ((f . n),r))) by A1;

          hence x in y by A13, A16, A17, XBOOLE_0:def 4;

        end;

        hence x in ( meet ( rng F)) by SETFAM_1:def 1;

      end;

      then (E /\ ( great_eq_dom (( inf f),r))) c= ( meet ( rng F));

      hence thesis by A8, XBOOLE_0:def 10;

    end;

    theorem :: MESFUNC8:17

    

     Th17: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real st (for n be Nat holds (F . n) = (( dom (f . 0 )) /\ ( great_dom ((f . n),r)))) holds for n be Nat holds (( superior_setsequence F) . n) = (( dom (f . 0 )) /\ ( great_dom ((( superior_realsequence f) . n),r)))

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real;

      set E = ( dom (f . 0 ));

      assume

       A1: for n be Nat holds (F . n) = (E /\ ( great_dom ((f . n),r)));

      let n be Nat;

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

      set f1 = (f ^\ n9);

      set F1 = (F ^\ n9);

       A2:

      now

        let k be Nat;

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

        (F1 . k) = (F . (n + k9)) by NAT_1:def 3;

        then (F1 . k) = (E /\ ( great_dom ((f . (n + k9)),r))) by A1;

        hence (F1 . k) = (E /\ ( great_dom ((f1 . k),r))) by NAT_1:def 3;

      end;

      

       A3: ( union ( rng (F ^\ n9))) = (( superior_setsequence F) . n) by Th2;

      consider g be sequence of ( PFuncs (X, ExtREAL )) such that

       A4: f = g and (f ^\ n9) = (g ^\ n9);

      (f1 . 0 ) = (g . (n + 0 qua Nat)) by A4, NAT_1:def 3;

      then ( dom (f1 . 0 )) = E by A4, Def2;

      then ( union ( rng F1)) = (E /\ ( great_dom (( sup f1),r))) by A2, Th15;

      hence thesis by A3, Th9;

    end;

    theorem :: MESFUNC8:18

    

     Th18: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real st (for n be Nat holds (F . n) = (( dom (f . 0 )) /\ ( great_eq_dom ((f . n),r)))) holds for n be Nat holds (( inferior_setsequence F) . n) = (( dom (f . 0 )) /\ ( great_eq_dom ((( inferior_realsequence f) . n),r)))

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real;

      set E = ( dom (f . 0 ));

      assume that

       A1: for n be Nat holds (F . n) = (E /\ ( great_eq_dom ((f . n),r)));

      let n be Nat;

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

      set f1 = (f ^\ n9);

      set F1 = (F ^\ n9);

       A2:

      now

        let k be Nat;

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

        (F1 . k) = (F . (n + k9)) by NAT_1:def 3;

        then (F1 . k) = (E /\ ( great_eq_dom ((f . (n + k9)),r))) by A1;

        hence (F1 . k) = (E /\ ( great_eq_dom ((f1 . k),r))) by NAT_1:def 3;

      end;

      

       A3: ( meet ( rng (F ^\ n9))) = (( inferior_setsequence F) . n) by Th2;

      consider g be sequence of ( PFuncs (X, ExtREAL )) such that

       A4: f = g and (f ^\ n9) = (g ^\ n9);

      (f1 . 0 ) = (g . (n + 0 qua Nat)) by A4, NAT_1:def 3;

      then ( dom (f1 . 0 )) = E by A4, Def2;

      then ( meet ( rng F1)) = (E /\ ( great_eq_dom (( inf f1),r))) by A2, Th16;

      hence thesis by A3, Th8;

    end;

    theorem :: MESFUNC8:19

    

     Th19: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) holds for n holds (( superior_realsequence f) . n) is E -measurable

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: ( dom (f . 0 )) = E and

       A2: for n be Nat holds (f . n) is E -measurable;

      let n;

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

       A3:

      now

        let r be Real;

        deffunc G( Element of NAT ) = (E /\ ( great_dom ((f . $1),r)));

        consider F be sequence of ( bool X) such that

         A4: for x be Element of NAT holds (F . x) = G(x) from FUNCT_2:sch 4;

        now

          let i be Nat;

          

           A5: (f . i) is E -measurable by A2;

          i in NAT by ORDINAL1:def 12;

          then

           A6: (F . i) = (E /\ ( great_dom ((f . i),r))) by A4;

          ( dom (f . i)) = E by A1, Def2;

          hence (F . i) in S by A6, A5, MESFUNC1: 29;

        end;

        then

         A7: ( rng F) c= S by NAT_1: 52;

        

         A8: for x be Nat holds (F . x) = (E /\ ( great_dom ((f . x),r)))

        proof

          let x be Nat;

          reconsider x9 = x as Element of NAT by ORDINAL1:def 12;

          (F . x9) = (E /\ ( great_dom ((f . x9),r))) by A4;

          hence thesis;

        end;

        reconsider F as SetSequence of S by A7, RELAT_1:def 19;

        (( superior_setsequence F) . n9) in ( rng ( superior_setsequence F)) by NAT_1: 51;

        then (( superior_setsequence F) . n9) in S;

        hence (E /\ ( great_dom ((( superior_realsequence f) . n),r))) in S by A1, A8, Th17;

      end;

      ( dom (( superior_realsequence f) . n9)) = E by A1, Def6;

      hence thesis by A3, MESFUNC1: 29;

    end;

    theorem :: MESFUNC8:20

    

     Th20: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) holds for n be Nat holds (( inferior_realsequence f) . n) is E -measurable

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: ( dom (f . 0 )) = E and

       A2: for n be Nat holds (f . n) is E -measurable;

      let n be Nat;

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

       A3:

      now

        let r be Real;

        deffunc G( Element of NAT ) = (E /\ ( great_eq_dom ((f . $1),r)));

        consider F be sequence of ( bool X) such that

         A4: for x be Element of NAT holds (F . x) = G(x) from FUNCT_2:sch 4;

        now

          let i be Nat;

          

           A5: (f . i) is E -measurable by A2;

          i in NAT by ORDINAL1:def 12;

          then

           A6: (F . i) = (E /\ ( great_eq_dom ((f . i),r))) by A4;

          ( dom (f . i)) = E by A1, Def2;

          hence (F . i) in S by A6, A5, MESFUNC1: 27;

        end;

        then

         A7: ( rng F) c= S by NAT_1: 52;

        

         A8: for x be Nat holds (F . x) = (E /\ ( great_eq_dom ((f . x),r)))

        proof

          let x be Nat;

          reconsider x9 = x as Element of NAT by ORDINAL1:def 12;

          (F . x9) = (E /\ ( great_eq_dom ((f . x9),r))) by A4;

          hence thesis;

        end;

        reconsider F as SetSequence of S by A7, RELAT_1:def 19;

        (( inferior_setsequence F) . n9) in ( rng ( inferior_setsequence F)) by NAT_1: 51;

        then (( inferior_setsequence F) . n9) in S;

        hence (E /\ ( great_eq_dom ((( inferior_realsequence f) . n),r))) in S by A1, A8, Th18;

      end;

      ( dom (( inferior_realsequence f) . n9)) = E by A1, Def5;

      hence thesis by A3, MESFUNC1: 27;

    end;

    theorem :: MESFUNC8:21

    

     Th21: for f be Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real st (for n be Nat holds (F . n) = (( dom (f . 0 )) /\ ( great_eq_dom ((( superior_realsequence f) . n),r)))) holds ( meet F) = (( dom (f . 0 )) /\ ( great_eq_dom (( lim_sup f),r)))

    proof

      let f be Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real;

      set E = ( dom (f . 0 ));

      set g = ( superior_realsequence f);

      assume

       A1: for n be Nat holds (F . n) = (E /\ ( great_eq_dom ((g . n),r)));

      ( dom (g . 0 )) = ( dom (f . 0 )) by Def6;

      then ( meet ( rng F)) = (E /\ ( great_eq_dom (( inf g),r))) by A1, Th16;

      hence thesis by Th12;

    end;

    theorem :: MESFUNC8:22

    

     Th22: for f be Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real st (for n be Nat holds (F . n) = (( dom (f . 0 )) /\ ( great_dom ((( inferior_realsequence f) . n),r)))) holds ( union ( rng F)) = (( dom (f . 0 )) /\ ( great_dom (( lim_inf f),r)))

    proof

      let f be Functional_Sequence of X, ExtREAL , F be SetSequence of S, r be Real;

      set E = ( dom (f . 0 ));

      set g = ( inferior_realsequence f);

      assume

       A1: for n be Nat holds (F . n) = (E /\ ( great_dom ((g . n),r)));

      ( dom (g . 0 )) = ( dom (f . 0 )) by Def5;

      then ( union ( rng F)) = (E /\ ( great_dom (( sup g),r))) by A1, Th15;

      hence thesis by Th11;

    end;

    theorem :: MESFUNC8:23

    

     Th23: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) holds ( lim_sup f) is E -measurable

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: ( dom (f . 0 )) = E and

       A2: for n be Nat holds (f . n) is E -measurable;

       A3:

      now

        let r be Real;

        deffunc G( Element of NAT ) = (E /\ ( great_eq_dom ((( superior_realsequence f) . $1),r)));

        consider F be sequence of ( bool X) such that

         A4: for x be Element of NAT holds (F . x) = G(x) from FUNCT_2:sch 4;

        now

          let i be Nat;

          

           A5: ( dom (( superior_realsequence f) . i)) = ( dom (f . 0 )) by Def6;

          i in NAT by ORDINAL1:def 12;

          then

           A6: (F . i) = (E /\ ( great_eq_dom ((( superior_realsequence f) . i),r))) by A4;

          (( superior_realsequence f) . i) is E -measurable by A1, A2, Th19;

          hence (F . i) in S by A1, A6, A5, MESFUNC1: 27;

        end;

        then

         A7: ( rng F) c= S by NAT_1: 52;

        

         A8: for x be Nat holds (F . x) = (E /\ ( great_eq_dom ((( superior_realsequence f) . x),r)))

        proof

          let x be Nat;

          reconsider x9 = x as Element of NAT by ORDINAL1:def 12;

          (F . x9) = (E /\ ( great_eq_dom ((( superior_realsequence f) . x9),r))) by A4;

          hence thesis;

        end;

        reconsider F as SetSequence of S by A7, RELAT_1:def 19;

        ( rng F) c= S;

        then F is sequence of S by FUNCT_2: 6;

        then

         A9: ( rng F) is N_Sub_set_fam of X by MEASURE1: 23;

        

         A10: ( rng F) is N_Measure_fam of S by A9, MEASURE2:def 1;

        ( meet F) = (E /\ ( great_eq_dom (( lim_sup f),r))) by A1, A8, Th21;

        hence (E /\ ( great_eq_dom (( lim_sup f),r))) in S by A10, MEASURE2: 2;

      end;

      ( dom ( lim_sup f)) = ( dom (f . 0 )) by Def8;

      hence thesis by A1, A3, MESFUNC1: 27;

    end;

    theorem :: MESFUNC8:24

    for f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) holds ( lim_inf f) is E -measurable

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S;

      assume that

       A1: ( dom (f . 0 )) = E and

       A2: for n be Nat holds (f . n) is E -measurable;

       A3:

      now

        let r be Real;

        deffunc G( Element of NAT ) = (E /\ ( great_dom ((( inferior_realsequence f) . $1),r)));

        consider F be sequence of ( bool X) such that

         A4: for x be Element of NAT holds (F . x) = G(x) from FUNCT_2:sch 4;

        now

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          then

           A5: (F . i) = (E /\ ( great_dom ((( inferior_realsequence f) . i),r))) by A4;

          

           A6: ( dom (( inferior_realsequence f) . i)) = E by A1, Def5;

          (( inferior_realsequence f) . i) is E -measurable by A1, A2, Th20;

          hence (F . i) in S by A5, A6, MESFUNC1: 29;

        end;

        then

         A7: ( rng F) c= S by NAT_1: 52;

        

         A8: for x be Nat holds (F . x) = (E /\ ( great_dom ((( inferior_realsequence f) . x),r)))

        proof

          let x be Nat;

          reconsider x9 = x as Element of NAT by ORDINAL1:def 12;

          (F . x9) = (E /\ ( great_dom ((( inferior_realsequence f) . x9),r))) by A4;

          hence thesis;

        end;

        reconsider F as SetSequence of S by A7, RELAT_1:def 19;

        ( rng F) c= S;

        then F is sequence of S by FUNCT_2: 6;

        then

         A9: ( rng F) is N_Sub_set_fam of X by MEASURE1: 23;

        

         A10: ( rng F) is N_Measure_fam of S by A9, MEASURE2:def 1;

        ( union ( rng F)) = (E /\ ( great_dom (( lim_inf f),r))) by A1, A8, Th22;

        hence (E /\ ( great_dom (( lim_inf f),r))) in S by A10, MEASURE2: 2;

      end;

      ( dom ( lim_inf f)) = E by A1, Def7;

      hence thesis by A3, MESFUNC1: 29;

    end;

    theorem :: MESFUNC8:25

    

     Th25: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) & (for x be Element of X st x in E holds (f # x) is convergent) holds ( lim f) is E -measurable

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , E be Element of S;

      assume

       A1: ( dom (f . 0 )) = E;

      then

       A2: ( dom ( lim_sup f)) = E by Def8;

      assume that

       A3: for n be Nat holds (f . n) is E -measurable and

       A4: for x be Element of X st x in E holds (f # x) is convergent;

      

       A5: ( dom ( lim f)) = E by A1, Def9;

       A6:

      now

        let x be Element of X;

        assume

         A7: x in ( dom ( lim f));

        then (f # x) is convergent by A5, A4;

        hence (( lim f) . x) = (( lim_sup f) . x) by A7, Th14;

      end;

      ( lim_sup f) is E -measurable by A1, A3, Th23;

      hence thesis by A5, A2, A6, PARTFUN1: 5;

    end;

    theorem :: MESFUNC8:26

    

     Th26: for f be with_the_same_dom Functional_Sequence of X, ExtREAL , g be PartFunc of X, ExtREAL , E be Element of S st ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable) & ( dom g) = E & for x be Element of X st x in E holds (f # x) is convergent & (g . x) = ( lim (f # x)) holds g is E -measurable

    proof

      let f be with_the_same_dom Functional_Sequence of X, ExtREAL , g be PartFunc of X, ExtREAL , E be Element of S;

      assume that

       A1: ( dom (f . 0 )) = E and

       A2: for n be Nat holds (f . n) is E -measurable and

       A3: ( dom g) = E and

       A4: for x be Element of X st x in E holds (f # x) is convergent & (g . x) = ( lim (f # x));

      

       A5: ( dom ( lim f)) = E by A1, Def9;

      now

        let x be Element of X;

        assume

         A6: x in ( dom ( lim f));

        then (g . x) = ( lim (f # x)) by A4, A5;

        hence (g . x) = (( lim f) . x) by A6, Def9;

      end;

      then

       A7: g = ( lim f) by A3, A5, PARTFUN1: 5;

      for x be Element of X st x in E holds (f # x) is convergent by A4;

      hence thesis by A1, A2, A7, Th25;

    end;

    theorem :: MESFUNC8:27

    

     Th27: for f be Functional_Sequence of X, ExtREAL , g be PartFunc of X, ExtREAL st for x be Element of X st x in ( dom g) holds (f # x) is convergent_to_finite_number & (g . x) = ( lim (f # x)) holds g is real-valued

    proof

      let f be Functional_Sequence of X, ExtREAL , g be PartFunc of X, ExtREAL ;

      assume

       A1: for x be Element of X st x in ( dom g) holds (f # x) is convergent_to_finite_number & (g . x) = ( lim (f # x));

      now

        let x be Element of X;

        assume

         A2: x in ( dom g);

        then

         A3: not (( lim (f # x)) = +infty & (f # x) is convergent_to_+infty) by A1, MESFUNC5: 50;

        (f # x) is convergent_to_finite_number by A1, A2;

        then

         A4: (f # x) is convergent by MESFUNC5:def 11;

         not (( lim (f # x)) = -infty & (f # x) is convergent_to_-infty) by A1, A2, MESFUNC5: 51;

        then

        consider g0 be Real such that

         A5: ( lim (f # x)) = g0 and for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.(((f # x) . m) - ( lim (f # x))).| < p and (f # x) is convergent_to_finite_number by A4, A3, MESFUNC5:def 12;

         |.(g . x).| = |.g0 qua Complex.| by A1, A2, A5, EXTREAL1: 12;

        hence |.(g . x).| < +infty by XXREAL_0: 9, XREAL_0:def 1;

      end;

      hence thesis by MESFUNC2:def 1;

    end;

    begin

    theorem :: MESFUNC8:28

    

     Th28: for M be sigma_Measure of S, f be with_the_same_dom Functional_Sequence of X, ExtREAL , g be PartFunc of X, ExtREAL , E be Element of S st (M . E) < +infty & ( dom (f . 0 )) = E & (for n be Nat holds (f . n) is E -measurable & (f . n) is real-valued) & ( dom g) = E & for x be Element of X st x in E holds (f # x) is convergent_to_finite_number & (g . x) = ( lim (f # x)) holds for r,e be Real st 0 < r & 0 < e holds ex H be Element of S, N be Nat st H c= E & (M . H) < r & for k be Nat st N < k holds for x be Element of X st x in (E \ H) holds |.(((f . k) . x) - (g . x)).| < e

    proof

      let M be sigma_Measure of S, f be with_the_same_dom Functional_Sequence of X, ExtREAL , g be PartFunc of X, ExtREAL , E be Element of S;

      assume that

       A1: (M . E) < +infty and

       A2: ( dom (f . 0 )) = E and

       A3: for n be Nat holds (f . n) is E -measurable & (f . n) is real-valued and

       A4: ( dom g) = E and

       A5: for x be Element of X st x in E holds (f # x) is convergent_to_finite_number & (g . x) = ( lim (f # x));

      let r,e be Real;

      defpred P[ Element of NAT , set] means $2 = (E /\ ( less_dom ( |.((f . $1) - g).|,e)));

      

       A6: g is real-valued by A4, A5, Th27;

      for x be Element of X st x in E holds (f # x) is convergent & (g . x) = ( lim (f # x))

      proof

        let x be Element of X;

        assume

         A7: x in E;

        then (f # x) is convergent_to_finite_number by A5;

        hence (f # x) is convergent by MESFUNC5:def 11;

        thus thesis by A5, A7;

      end;

      then

       A8: g is E -measurable by A2, A3, A4, Th26;

      

       A9: for n be Element of NAT holds |.((f . n) - g).| is E -measurable & ( dom ((f . n) - g)) = E & ( dom |.((f . n) - g).|) = E

      proof

        let n be Element of NAT ;

        

         A10: (f . n) is real-valued by A3;

        ( dom ((f . n) - g)) = (( dom (f . n)) /\ ( dom g)) by A6, MESFUNC2: 2;

        then

         A11: ( dom ((f . n) - g)) = (E /\ E) by A2, A4, Def2;

        (f . n) is E -measurable by A3;

        then ((f . n) - g) is E -measurable by A4, A8, A6, A10, MESFUNC2: 11;

        hence thesis by A11, MESFUNC1:def 10, MESFUNC2: 27;

      end;

      

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

      proof

        let n be Element of NAT ;

         |.((f . n) - g).| is E -measurable by A9;

        then (E /\ ( less_dom ( |.((f . n) - g).|,e))) in S by MESFUNC1:def 16;

        hence thesis;

      end;

      consider K be sequence of S such that

       A13: for n be Element of NAT holds P[n, (K . n)] from FUNCT_2:sch 3( A12);

      defpred Q[ Nat, set] means $2 = { x where x be Element of X : for k st $1 <= k holds x in (K . k) };

      

       A14: for n be Element of NAT holds ex Z be Element of S st Q[n, Z]

      proof

        let n be Element of NAT ;

        take { x where x be Element of X : for k st n <= k holds x in (K . k) };

        thus thesis by Th1;

      end;

      consider EN be sequence of S such that

       A15: for n be Element of NAT holds Q[n, (EN . n)] from FUNCT_2:sch 3( A14);

      

       A16: for n be Nat holds Q[n, (EN . n)]

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A15;

      end;

      

       A17: 0. <= (M . E) by MEASURE1:def 2;

      then

      reconsider ME = (M . E) as Element of REAL by A1, XXREAL_0: 14;

      defpred R[ Element of NAT , set] means $2 = (M . (EN . $1));

      

       A18: for n be Nat holds (EN . n) c= E & (M . (EN . n)) <= (M . E) & (M . (EN . n)) is Element of REAL & (M . (E \ (EN . n))) = ((M . E) - (M . (EN . n))) & (M . (E \ (EN . n))) is Element of REAL

      proof

        reconsider r1 = (M . E) as Element of REAL by A1, A17, XXREAL_0: 14;

        let n be Nat;

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

        thus

         A19: (EN . n) c= E

        proof

          let z be object;

          assume z in (EN . n);

          then z in { x where x be Element of X : for k st n9 <= k holds x in (K . k) } by A16;

          then ex x be Element of X st z = x & for k st n <= k holds x in (K . k);

          then z in (K . n);

          then z in (E /\ ( less_dom ( |.((f . n9) - g).|,e))) by A13;

          hence thesis by XBOOLE_0:def 4;

        end;

        hence

         A20: (M . (EN . n)) <= (M . E) by MEASURE1: 31;

        

         A21: -infty < (M . (EN . n)) by MEASURE1:def 2;

        then

        reconsider r2 = (M . (EN . n)) as Element of REAL by A1, A20, XXREAL_0: 14;

        thus (M . (EN . n)) is Element of REAL by A1, A20, A21, XXREAL_0: 14;

        thus (M . (E \ (EN . n))) = ((M . E) - (M . (EN . n))) by A1, A19, A20, MEASURE1: 32, XXREAL_0: 4;

        ((M . E) - (M . (EN . n))) = (r1 - r2) by SUPINF_2: 3;

        hence thesis by A19, MEASURE1: 32, XXREAL_0: 4;

      end;

       A22:

      now

        let n be Element of NAT ;

        (M . (EN . n)) is Element of REAL by A18;

        hence ex y be Element of REAL st R[n, y];

      end;

      consider seq1 be Real_Sequence such that

       A23: for n be Element of NAT holds R[n, (seq1 . n)] from FUNCT_2:sch 3( A22);

      assume

       A24: 0 < r;

      assume

       A25: 0 < e;

      

       A26: E c= ( union ( rng EN))

      proof

        let z be object;

        assume

         A27: z in E;

        then

        reconsider x = z as Element of X;

        

         A28: not (( lim (f # x)) = +infty & (f # x) is convergent_to_+infty) by A5, A27, MESFUNC5: 50;

        (f # x) is convergent_to_finite_number by A5, A27;

        then

         A29: (f # x) is convergent by MESFUNC5:def 11;

         not (( lim (f # x)) = -infty & (f # x) is convergent_to_-infty) by A5, A27, MESFUNC5: 51;

        then ex g be Real st ( lim (f # x)) = g & (for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.(((f # x) . m) - ( lim (f # x))).| < p) & (f # x) is convergent_to_finite_number by A29, A28, MESFUNC5:def 12;

        then

        consider n be Nat such that

         A30: for m be Nat st n <= m holds |.(((f # x) . m) - ( lim (f # x))).| < e by A25;

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

        

         A31: (g . x) = ( lim (f # x)) by A5, A27;

        now

          let k;

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

          

           A32: ( dom |.((f . k9) - g).|) = E by A9;

          assume n0 <= k;

          then |.(((f # x) . k) - ( lim (f # x))).| < e by A30;

          then

           A33: |.(((f . k) . x) - (g . x)).| < e by A31, MESFUNC5:def 13;

          ( dom ((f . k9) - g)) = E by A9;

          then |.(((f . k) - g) . x).| < e by A27, A33, MESFUNC1:def 4;

          then ( |.((f . k) - g).| . x) < e by A27, A32, MESFUNC1:def 10;

          then x in ( less_dom ( |.((f . k) - g).|,e)) by A27, A32, MESFUNC1:def 11;

          then x in (E /\ ( less_dom ( |.((f . k) - g).|,e))) by A27, XBOOLE_0:def 4;

          then x in (K . k9) by A13;

          hence x in (K . k);

        end;

        then x in { y where y be Element of X : for k st n0 <= k holds y in (K . k) };

        then

         A34: x in (EN . n0) by A16;

        (EN . n0) in ( rng EN) by FUNCT_2: 4;

        hence thesis by A34, TARSKI:def 4;

      end;

      defpred U[ Element of NAT , set] means $2 = (M . (E \ (EN . $1)));

      

       A35: ( dom (M * EN)) = NAT by FUNCT_2:def 1;

      

       A36: for n,m be Nat st n <= m holds (EN . n) c= (EN . m) & (M . (EN . n)) <= (M . (EN . m))

      proof

        let n,m be Nat;

        assume

         A37: n <= m;

        thus (EN . n) c= (EN . m)

        proof

          let z be object;

          assume z in (EN . n);

          then z in { x where x be Element of X : for k st n <= k holds x in (K . k) } by A16;

          then

           A38: ex x be Element of X st z = x & for k st n <= k holds x in (K . k);

          then for k st m <= k holds z in (K . k) by A37, XXREAL_0: 2;

          then z in { y where y be Element of X : for k st m <= k holds y in (K . k) } by A38;

          hence thesis by A16;

        end;

        hence thesis by MEASURE1: 31;

      end;

      set seq3 = ( NAT --> ME);

      

       A39: for n be Nat holds (seq3 . n) = ME by ORDINAL1:def 12, FUNCOP_1: 7;

      then

       A40: seq3 is constant by VALUED_0:def 18;

       A41:

      now

        let x be object;

        assume

         A42: x in ( dom (M * EN));

        then

        reconsider n = x as Element of NAT ;

        ((M * EN) . x) = (M . (EN . n)) by A42, FUNCT_1: 12;

        hence ((M * EN) . x) = (seq1 . x) by A23;

      end;

      ( dom seq1) = NAT by FUNCT_2:def 1;

      then

       A43: (M * EN) = seq1 by A35, A41, FUNCT_1: 2;

      now

        let y be set;

        assume y in ( rng EN);

        then

        consider x be object such that

         A44: x in NAT and

         A45: y = (EN . x) by FUNCT_2: 11;

        reconsider x9 = x as Nat by A44;

        y = (EN . x9) by A45;

        hence y c= E by A18;

      end;

      then ( union ( rng EN)) c= E by ZFMISC_1: 76;

      then

       A46: ( union ( rng EN)) = E by A26, XBOOLE_0:def 10;

      

       A47: seq1 is convergent & ( lim seq1) = (M . E)

      proof

        reconsider r1 = (M . E) as Element of REAL by A1, A17, XXREAL_0: 14;

        

         A48: for n be Nat holds (EN . n) c= (EN . (n + 1))

        proof

          let n be Nat;

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

          hence thesis by A36;

        end;

         A49:

        now

          let n be Nat;

          

           A50: n in NAT by ORDINAL1:def 12;

          (M . (EN . n)) <= (M . E) by A18;

          then

           A51: (seq1 . n) <= r1 by A23, A50;

          (r1 + 0 qua Nat) < (r1 + 1) by XREAL_1: 8;

          hence (seq1 . n) < (r1 + 1) by A51, XXREAL_0: 2;

        end;

        then

         A52: seq1 is bounded_above by SEQ_2:def 3;

        consider r be Real such that

         A53: for n be Nat holds (seq1 . n) < r by A49;

        r is UpperBound of ( rng seq1)

        proof

          let d be ExtReal;

          assume d in ( rng seq1);

          then ex x be object st x in NAT & d = (seq1 . x) by FUNCT_2: 11;

          hence d <= r by A53;

        end;

        then ( rng seq1) is bounded_above;

        then

         A54: ( sup ( rng (M * EN))) = ( upper_bound ( rng seq1)) by A43, RINFSUP2: 1;

        now

          let n,m be Nat;

          assume

           A55: n <= m;

          

           A56: n in NAT by ORDINAL1:def 12;

          

           A57: m in NAT by ORDINAL1:def 12;

          

           A58: (seq1 . m) = (M . (EN . m)) by A23, A57;

          (seq1 . n) = (M . (EN . n)) by A23, A56;

          hence (seq1 . n) <= (seq1 . m) by A36, A55, A58;

        end;

        then

         A59: seq1 is non-decreasing by SEQM_3: 6;

        hence seq1 is convergent by A52;

        ( lim seq1) = ( upper_bound seq1) by A59, A52, RINFSUP1: 24;

        hence thesis by A46, A54, A48, MEASURE2: 23;

      end;

       A60:

      now

        let n be Element of NAT ;

        (M . (E \ (EN . n))) is Element of REAL by A18;

        hence ex y be Element of REAL st U[n, y];

      end;

      consider seq2 be Real_Sequence such that

       A61: for n be Element of NAT holds U[n, (seq2 . n)] from FUNCT_2:sch 3( A60);

      now

        let n be Nat;

        

         A62: n in NAT by ORDINAL1:def 12;

        (seq2 . n) = (M . (E \ (EN . n))) by A61, A62;

        then

         A63: (seq2 . n) = ((M . E) - (M . (EN . n))) by A18;

        (M . (EN . n)) = (seq1 . n) by A23, A62;

        then (seq2 . n) = (ME - (seq1 . n)) by A63, SUPINF_2: 3;

        then (seq2 . n) = ((seq3 . n) - (seq1 . n)) by A39;

        hence (seq2 . n) = ((seq3 . n) + (( - seq1) . n)) by SEQ_1: 10;

      end;

      then

       A64: seq2 = (seq3 - seq1) by SEQ_1: 7;

      then

       A65: seq2 is convergent by A47, A40;

      

       A66: (seq3 . 0 ) = ME by A39;

      ( lim seq2) = (( lim seq3) - ( lim seq1)) by A47, A64, A40, SEQ_2: 12;

      then ( lim seq2) = (ME - ME) by A47, A40, A66, SEQ_4: 25;

      then

      consider N be Nat such that

       A67: for m be Nat st N <= m holds |.((seq2 . m) - 0 ) qua Complex.| < r by A24, A65, SEQ_2:def 7;

      reconsider H = (E \ (EN . N)) as Element of S;

      

       A68: (E \ H) = (E /\ (EN . N)) by XBOOLE_1: 48;

      (EN . N) c= E by A18;

      then

       A69: (E \ H) = (EN . N) by A68, XBOOLE_1: 28;

      

       A70: for k be Nat st N < k holds for x be Element of X st x in (E \ H) holds |.(((f . k) . x) - (g . x)).| < e

      proof

        let k be Nat;

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

        assume

         A71: N < k;

        let x be Element of X;

        assume x in (E \ H);

        then x in { y where y be Element of X : for k st N <= k holds y in (K . k) } by A16, A69;

        then ex y be Element of X st x = y & for k st N <= k holds y in (K . k);

        then x in (K . k) by A71;

        then

         A72: x in (E /\ ( less_dom ( |.((f . k9) - g).|,e))) by A13;

        then

         A73: x in E by XBOOLE_0:def 4;

        x in ( less_dom ( |.((f . k) - g).|,e)) by A72, XBOOLE_0:def 4;

        then

         A74: ( |.((f . k) - g).| . x) < e by MESFUNC1:def 11;

        

         A75: ( dom ((f . k9) - g)) = E by A9;

        ( dom |.((f . k9) - g).|) = E by A9;

        then |.(((f . k) - g) . x).| < e by A73, A74, MESFUNC1:def 10;

        hence thesis by A73, A75, MESFUNC1:def 4;

      end;

      take H, N;

      

       A76: N in NAT by ORDINAL1:def 12;

      (M . (E \ (EN . N))) = (seq2 . N) by A61, A76;

      then

       A77: 0 <= (seq2 . N) by MEASURE1:def 2;

       |.((seq2 . N) - 0 ) qua Complex.| < r by A67;

      then (seq2 . N) < r by A77, ABSVALUE:def 1;

      hence thesis by A61, A70, XBOOLE_1: 36, A76;

    end;

    theorem :: MESFUNC8:29

    for X,Y be non empty set, E be set, F,G be Function of X, Y st for x be Element of X holds (G . x) = (E \ (F . x)) holds ( union ( rng G)) = (E \ ( meet ( rng F)))

    proof

      let X,Y be non empty set, E be set, F,G be Function of X, Y;

      assume

       A1: for x be Element of X holds (G . x) = (E \ (F . x));

      

       A2: ( dom G) = X by FUNCT_2:def 1;

      now

        let Z be object;

        assume Z in ( DIFFERENCE ( {E},( rng F)));

        then

        consider X1,Y be set such that

         A3: X1 in {E} and

         A4: Y in ( rng F) and

         A5: Z = (X1 \ Y) by SETFAM_1:def 6;

        consider x be object such that

         A6: x in ( dom F) and

         A7: Y = (F . x) by A4, FUNCT_1:def 3;

        reconsider x as Element of X by A6;

        X1 = E by A3, TARSKI:def 1;

        then Z = (G . x) by A1, A5, A7;

        hence Z in ( rng G) by A2, FUNCT_1: 3;

      end;

      then

       A8: ( DIFFERENCE ( {E},( rng F))) c= ( rng G);

      

       A9: ( dom F) = X by FUNCT_2:def 1;

      now

        let Z be object;

        

         A10: E in {E} by TARSKI:def 1;

        assume Z in ( rng G);

        then

        consider x be object such that

         A11: x in ( dom G) and

         A12: Z = (G . x) by FUNCT_1:def 3;

        reconsider x as Element of X by A11;

        

         A13: (F . x) in ( rng F) by A9, FUNCT_1: 3;

        Z = (E \ (F . x)) by A1, A12;

        hence Z in ( DIFFERENCE ( {E},( rng F))) by A13, A10, SETFAM_1:def 6;

      end;

      then ( rng G) c= ( DIFFERENCE ( {E},( rng F)));

      then ( DIFFERENCE ( {E},( rng F))) = ( rng G) by A8, XBOOLE_0:def 10;

      hence thesis by SETFAM_1: 27;

    end;

    reconsider jj = 1 as Real;

    ::$Notion-Name

    theorem :: MESFUNC8:30

    for M be sigma_Measure of S, f be with_the_same_dom Functional_Sequence of X, ExtREAL , g be PartFunc of X, ExtREAL , E be Element of S st (( dom (f . 0 )) = E & for n be Nat holds (f . n) is E -measurable) & (M . E) < +infty & (for n be Nat holds ex L be Element of S st L c= E & (M . (E \ L)) = 0 & for x be Element of X st x in L holds |.((f . n) . x).| < +infty ) & ex G be Element of S st G c= E & (M . (E \ G)) = 0 & (for x be Element of X st x in E holds (f # x) is convergent_to_finite_number) & ( dom g) = E & (for x be Element of X st x in G holds (g . x) = ( lim (f # x))) holds for e be Real st 0 < e holds ex F be Element of S st F c= E & (M . (E \ F)) <= e & for p be Real st 0 < p holds ex N be Nat st for n be Nat st N < n holds for x be Element of X st x in F holds |.(((f . n) . x) - (g . x)).| < p

    proof

      let M be sigma_Measure of S, f be with_the_same_dom Functional_Sequence of X, ExtREAL , g be PartFunc of X, ExtREAL , E be Element of S such that

       A1: ( dom (f . 0 )) = E and

       A2: for n be Nat holds (f . n) is E -measurable and

       A3: (M . E) < +infty and

       A4: for n be Nat holds ex L be Element of S st L c= E & (M . (E \ L)) = 0 & for x be Element of X st x in L holds |.((f . n) . x).| < +infty and

       A5: ex G be Element of S st G c= E & (M . (E \ G)) = 0 & (for x be Element of X st x in E holds (f # x) is convergent_to_finite_number) & ( dom g) = E & for x be Element of X st x in G holds (g . x) = ( lim (f # x));

      defpred P[ Element of NAT , set] means $2 c= E & (M . (E \ $2)) = 0 & for x be Element of X st x in $2 holds |.((f . $1) . x).| < +infty ;

      

       A6: for n be Element of NAT holds ex Z be Element of S st P[n, Z] by A4;

      consider LN be sequence of S such that

       A7: for n be Element of NAT holds P[n, (LN . n)] from FUNCT_2:sch 3( A6);

      ( rng LN) is N_Sub_set_fam of X by MEASURE1: 23;

      then ( rng LN) is N_Measure_fam of S by MEASURE2:def 1;

      then

      reconsider MRLN = ( meet ( rng LN)) as Element of S by MEASURE2: 2;

      let e0 be Real;

      assume

       A8: 0 < e0;

      set e = (e0 / 2);

      consider G be Element of S such that

       A9: G c= E and

       A10: (M . (E \ G)) = 0 and

       A11: for x be Element of X st x in E holds (f # x) is convergent_to_finite_number and

       A12: ( dom g) = E and

       A13: for x be Element of X st x in G holds (g . x) = ( lim (f # x)) by A5;

      (MRLN /\ G) is Element of S;

      then

      reconsider L = (( meet ( rng LN)) /\ G) as Element of S;

      set gL = (g | L);

      

       A14: L c= G by XBOOLE_1: 17;

      then (M . L) <= (M . E) by A9, MEASURE1: 31, XBOOLE_1: 1;

      then

       A15: (M . L) < +infty by A3, XXREAL_0: 2;

      ( dom gL) = (( dom g) /\ L) by RELAT_1: 61;

      then

       A16: ( dom gL) = L by A9, A12, A14, XBOOLE_1: 1, XBOOLE_1: 28;

      deffunc FNL( Nat) = ((f . $1) | L);

      consider fL be Functional_Sequence of X, ExtREAL such that

       A17: for n be Nat holds (fL . n) = FNL(n) from SEQFUNC:sch 1;

      for n,m be Nat holds ( dom (fL . n)) = ( dom (fL . m))

      proof

        let n,m be Nat;

        (fL . m) = ((f . m) | L) by A17;

        then

         A18: ( dom (fL . m)) = (( dom (f . m)) /\ L) by RELAT_1: 61;

        (fL . n) = ((f . n) | L) by A17;

        then ( dom (fL . n)) = (( dom (f . n)) /\ L) by RELAT_1: 61;

        hence thesis by A18, Def2;

      end;

      then

      reconsider fL as with_the_same_dom Functional_Sequence of X, ExtREAL by Def2;

      

       A19: L c= E by A9, A14;

      

       A20: for x be Element of X st x in L holds (fL # x) is convergent_to_finite_number & (gL . x) = ( lim (fL # x))

      proof

        let x be Element of X;

        

         A21: ( dom (fL # x)) = NAT by FUNCT_2:def 1;

        

         A22: ( dom (f # x)) = NAT by FUNCT_2:def 1;

        assume

         A23: x in L;

        

         A24: for y be object st y in NAT holds ((fL # x) . y) = ((f # x) . y)

        proof

          let y be object;

          assume y in NAT ;

          then

          reconsider n = y as Element of NAT ;

          (((f . n) | L) . x) = ((f . n) . x) by A23, FUNCT_1: 49;

          then

           A25: ((fL . n) . x) = ((f . n) . x) by A17;

          ((f . n) . x) = ((f # x) . n) by MESFUNC5:def 13;

          hence thesis by A25, MESFUNC5:def 13;

        end;

        then

         A26: (fL # x) = (f # x) by FUNCT_2: 12;

        (f # x) is convergent_to_finite_number by A11, A19, A23;

        hence (fL # x) is convergent_to_finite_number by A21, A22, A24, FUNCT_1: 2;

        L c= G by XBOOLE_1: 17;

        then (g . x) = ( lim (f # x)) by A13, A23;

        hence thesis by A23, A26, FUNCT_1: 49;

      end;

      defpred R[ Element of NAT , set] means $2 c= L & (M . $2) < ((e (#) ((1 / 2) GeoSeq )) . $1) & ex Np be Element of NAT st for k be Element of NAT st Np < k holds for x be Element of X st x in (L \ $2) holds |.(((fL . k) . x) - (gL . x)).| < (((1 / 2) GeoSeq ) . $1);

      

       A27: for n be Nat holds ( dom (fL . n)) = L & (fL . n) is L -measurable & (fL . n) is real-valued

      proof

        let n be Nat;

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

        

         A28: (fL . n) = ((f . n) | L) by A17;

        then

         A29: ( dom (fL . n)) = (( dom (f . n)) /\ L) by RELAT_1: 61;

        then ( dom (fL . n9)) = (E /\ L) by A1, Def2;

        hence

         A30: ( dom (fL . n)) = L by A9, A14, XBOOLE_1: 1, XBOOLE_1: 28;

        (f . n) is L -measurable by A2, A19, MESFUNC1: 30;

        hence (fL . n) is L -measurable by A28, A29, A30, MESFUNC5: 42;

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

        proof

          let x be Element of X;

          ( dom LN) = NAT by FUNCT_2:def 1;

          then

           A31: (LN . n9) in ( rng LN) by FUNCT_1: 3;

          assume

           A32: x in ( dom (fL . n));

          then x in ( meet ( rng LN)) by A30, XBOOLE_0:def 4;

          then x in (LN . n) by A31, SETFAM_1:def 1;

          then |.((f . n9) . x).| < +infty by A7;

          hence thesis by A28, A32, FUNCT_1: 47;

        end;

        hence thesis by MESFUNC2:def 1;

      end;

      then

       A33: ( dom (fL . 0 )) = L;

      

       A34: for p be Nat holds ex Hp be Element of S, Np be Nat st Hp c= L & (M . Hp) < ((e (#) ((1 / 2) GeoSeq )) . p) & for k be Nat st Np < k holds for x be Element of X st x in (L \ Hp) holds |.(((fL . k) . x) - (gL . x)).| < (((1 / 2) GeoSeq ) . p)

      proof

        let p be Nat;

        reconsider p9 = p as Element of NAT by ORDINAL1:def 12;

        

         A35: ((e (#) ((1 / 2) GeoSeq )) . p) = (e * (((1 / 2) GeoSeq ) . p9)) by SEQ_1: 9;

         0 < ((jj / 2) |^ p) by PREPOWER: 6;

        then

         A36: 0 < (((1 / 2) GeoSeq ) . p9) by PREPOWER:def 1;

         0 < ((jj / 2) |^ p) by PREPOWER: 6;

        then

         A37: 0 < (((1 / 2) GeoSeq ) . p9) by PREPOWER:def 1;

         0 < e by A8;

        then 0 < ((e (#) ((1 / 2) GeoSeq )) . p) by A36, A35, XREAL_1: 129;

        hence thesis by A15, A27, A33, A16, A20, A37, Th28;

      end;

      

       A38: for n be Element of NAT holds ex Z be Element of S st R[n, Z]

      proof

        let n be Element of NAT ;

        reconsider n9 = n as Nat;

        consider Z be Element of S, Np be Nat such that

         A39: Z c= L and

         A40: (M . Z) < ((e (#) ((1 / 2) GeoSeq )) . n9) and

         A41: for k be Nat st Np < k holds for x be Element of X st x in (L \ Z) holds |.(((fL . k) . x) - (gL . x)).| < (((1 / 2) GeoSeq ) . n9) by A34;

        reconsider Np9 = Np as Element of NAT by ORDINAL1:def 12;

        for k be Element of NAT st Np9 < k holds for x be Element of X st x in (L \ Z) holds |.(((fL . k) . x) - (gL . x)).| < (((1 / 2) GeoSeq ) . n9) by A41;

        hence thesis by A39, A40;

      end;

      consider HP be sequence of S such that

       A42: for p be Element of NAT holds R[p, (HP . p)] from FUNCT_2:sch 3( A38);

      defpred U[ Element of NAT , set] means $2 = (M . (HP . $1));

      

       A43: for n be Element of NAT holds ex y be Element of REAL st U[n, y]

      proof

        let n be Element of NAT ;

        

         A44: -infty < (M . (HP . n)) by MEASURE1:def 2;

        (M . (HP . n)) < ((e (#) ((1 / 2) GeoSeq )) . n) by A42;

        then (M . (HP . n)) in REAL by A44, XXREAL_0: 48;

        hence thesis;

      end;

      consider me be Real_Sequence such that

       A45: for p be Element of NAT holds U[p, (me . p)] from FUNCT_2:sch 3( A43);

      

       A46: for p be Element of NAT holds (me . p) <= ((e (#) ((1 / 2) GeoSeq )) . p)

      proof

        let p be Element of NAT ;

        (me . p) = (M . (HP . p)) by A45;

        hence thesis by A42;

      end;

      

       A47: for p be Nat holds 0 <= (me . p) & (me . p) <= ((e (#) ((1 / 2) GeoSeq )) . p)

      proof

        let p be Nat;

        

         A48: p in NAT by ORDINAL1:def 12;

         0. <= (M . (HP . p)) by MEASURE1:def 2;

        hence thesis by A45, A46, A48;

      end;

      then for p be Nat holds 0 <= (me . p) & (me . p) <= ((e (#) ((1 / 2) GeoSeq )) . p);

      then

       A49: me is nonnegative;

      deffunc ELN( Element of NAT ) = (E \ (LN . $1));

      consider ELN be sequence of S such that

       A50: for n be Element of NAT holds (ELN . n) = ELN(n) from FUNCT_2:sch 4;

      ( rng ELN) is N_Sub_set_fam of X by MEASURE1: 23;

      then

      reconsider RELN = ( rng ELN) as N_Measure_fam of S by MEASURE2:def 1;

      

       A51: (E /\ ( union ( rng HP))) c= ( union ( rng HP)) by XBOOLE_1: 17;

      for A be set st A in RELN holds A is measure_zero of M

      proof

        let A be set;

        assume A in RELN;

        then

        consider n be object such that

         A52: n in NAT and

         A53: A = (ELN . n) by FUNCT_2: 11;

        reconsider n as Element of NAT by A52;

        (M . (ELN . n)) = (M . (E \ (LN . n))) by A50

        .= 0 by A7;

        hence thesis by A53, MEASURE1:def 7;

      end;

      then ( union RELN) is measure_zero of M by MEASURE2: 14;

      then

       A54: (M . ( union RELN)) = 0. by MEASURE1:def 7;

      now

        let x be object;

        assume

         A55: x in (E \ ( meet ( rng LN)));

        then

         A56: x in E by XBOOLE_0:def 5;

         not x in ( meet ( rng LN)) by A55, XBOOLE_0:def 5;

        then

        consider Y be set such that

         A57: Y in ( rng LN) and

         A58: not x in Y by SETFAM_1:def 1;

        consider m be object such that

         A59: m in ( dom LN) and

         A60: Y = (LN . m) by A57, FUNCT_1:def 3;

        reconsider m as Element of NAT by A59;

        ( dom ELN) = NAT by FUNCT_2:def 1;

        then

         A61: (ELN . m) in ( rng ELN) by FUNCT_1: 3;

        (ELN . m) = (E \ (LN . m)) by A50;

        then x in (ELN . m) by A56, A58, A60, XBOOLE_0:def 5;

        hence x in ( union RELN) by A61, TARSKI:def 4;

      end;

      then

       A62: (E \ ( meet ( rng LN))) c= ( union RELN);

      now

        let x be object;

        assume x in ( union RELN);

        then

        consider Y be set such that

         A63: x in Y and

         A64: Y in RELN by TARSKI:def 4;

        consider m be object such that

         A65: m in ( dom ELN) and

         A66: (ELN . m) = Y by A64, FUNCT_1:def 3;

        reconsider m as Element of NAT by A65;

        ( dom LN) = NAT by FUNCT_2:def 1;

        then

         A67: (LN . m) in ( rng LN) by FUNCT_1: 3;

        

         A68: Y = (E \ (LN . m)) by A50, A66;

        then not x in (LN . m) by A63, XBOOLE_0:def 5;

        then

         A69: not x in ( meet ( rng LN)) by A67, SETFAM_1:def 1;

        x in E by A63, A68, XBOOLE_0:def 5;

        hence x in (E \ ( meet ( rng LN))) by A69, XBOOLE_0:def 5;

      end;

      then ( union RELN) c= (E \ ( meet ( rng LN)));

      then

       A70: ( union RELN) = (E \ ( meet ( rng LN))) by A62, XBOOLE_0:def 10;

      ( rng HP) is N_Sub_set_fam of X by MEASURE1: 23;

      then

       A71: ( rng HP) is N_Measure_fam of S by MEASURE2:def 1;

      reconsider MRHP = ( union ( rng HP)) as Element of S by MEASURE1: 24;

      (L \ MRHP) is Element of S;

      then

      consider F be Element of S such that

       A72: F = (L \ ( union ( rng HP)));

      (E \ L) = ((E \ ( meet ( rng LN))) \/ (E \ G)) by XBOOLE_1: 54;

      then (M . (E \ L)) <= ((M . ( union RELN)) + (M . (E \ G))) by A70, MEASURE1: 33;

      then (M . (E \ L)) <= 0. by A10, A54;

      then

       A73: (M . (E \ L)) = 0 by MEASURE1:def 2;

      reconsider MRHP = ( union ( rng HP)) as Element of S by MEASURE1: 24;

      

       A74: (M . ((E \ L) \/ MRHP)) <= ((M . (E \ L)) + (M . MRHP)) by MEASURE1: 33;

      (E \ F) = ((E \ L) \/ (E /\ ( union ( rng HP)))) by A72, XBOOLE_1: 52;

      then (M . (E \ F)) <= (M . ((E \ L) \/ MRHP)) by A51, MEASURE1: 31, XBOOLE_1: 9;

      then (M . (E \ F)) <= ((M . (E \ L)) + (M . MRHP)) by A74, XXREAL_0: 2;

      then

       A75: (M . (E \ F)) <= (M . MRHP) by A73, XXREAL_3: 4;

      ( dom me) = NAT by FUNCT_2:def 1;

      then

       A76: ( dom me) = ( dom (M * HP)) by FUNCT_2:def 1;

      

       A77: for x be object st x in ( dom me) holds (me . x) = ((M * HP) . x)

      proof

        let x be object;

        assume

         A78: x in ( dom me);

        then ((M * HP) . x) = (M . (HP . x)) by A76, FUNCT_1: 12;

        hence thesis by A45, A78;

      end;

      

       A79: |.(1 / 2) qua Complex.| = (1 / 2) by ABSVALUE:def 1;

      then

       A80: ((1 / 2) GeoSeq ) is summable by SERIES_1: 24;

      then

       A81: (e (#) ((1 / 2) GeoSeq )) is summable by SERIES_1: 10;

      then me is summable by A47, SERIES_1: 20;

      then ( Sum me) = ( SUM (M * HP)) by A49, A76, A77, FUNCT_1: 2, PROB_4: 12;

      then

       A82: (M . ( union ( rng HP))) <= ( Sum me) by A71, MEASURE2: 11;

      

       A83: for q be Real st 0 < q holds ex p be Element of NAT st (((1 / 2) GeoSeq ) . p) < q

      proof

        let q be Real;

        assume

         A84: 0 < q;

        

         A85: ( lim ((1 / 2) GeoSeq )) = 0 by A80, SERIES_1: 4;

        ((1 / 2) GeoSeq ) is convergent by A80, SERIES_1: 4;

        then

        consider p be Nat such that

         A86: for n be Nat st p <= n holds |.((((1 / 2) GeoSeq ) . n) - 0 ) qua Complex.| < q by A84, A85, SEQ_2:def 7;

        take p;

         0 < ((jj / 2) |^ p) by PREPOWER: 6;

        then

         A87: 0 <= (((1 / 2) GeoSeq ) . p) by PREPOWER:def 1;

        

         A88: p in NAT by ORDINAL1:def 12;

         |.((((1 / 2) GeoSeq ) . p) - 0 ) qua Complex.| < q by A86;

        hence thesis by A87, ABSVALUE:def 1, A88;

      end;

      

       A89: for x be Element of X st x in F holds for p be Element of NAT holds x in (L \ (HP . p))

      proof

        let x be Element of X;

        assume

         A90: x in F;

        let p be Element of NAT ;

        ( dom HP) = NAT by FUNCT_2:def 1;

        then (HP . p) in ( rng HP) by FUNCT_1: 3;

        then (L \ ( union ( rng HP))) c= (L \ (HP . p)) by XBOOLE_1: 34, ZFMISC_1: 74;

        hence thesis by A72, A90;

      end;

      

       A91: for q be Real st 0 < q holds ex N be Nat st for n be Nat st N < n holds for x be Element of X st x in F holds |.(((f . n) . x) - (g . x)).| < q

      proof

        let q be Real;

        assume 0 < q;

        then

        consider p be Element of NAT such that

         A92: (((1 / 2) GeoSeq ) . p) < q by A83;

        consider Np be Element of NAT such that

         A93: for k be Element of NAT st Np < k holds for x be Element of X st x in (L \ (HP . p)) holds |.(((fL . k) . x) - (gL . x)).| < (((1 / 2) GeoSeq ) . p) by A42;

        take Np;

        hereby

          let n be Nat;

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

          assume

           A94: Np < n;

          hereby

            let x be Element of X;

            

             A95: (fL . n) = ((f . n) | L) by A17;

            assume

             A96: x in F;

            then |.(((fL . n9) . x) - (gL . x)).| < (((1 / 2) GeoSeq ) . p) by A89, A93, A94;

            then

             A97: |.(((fL . n) . x) - (gL . x)).| < q by A92, XXREAL_0: 2;

            

             A98: F c= L by A72, XBOOLE_1: 36;

            then (gL . x) = (g . x) by A96, FUNCT_1: 49;

            hence |.(((f . n) . x) - (g . x)).| < q by A96, A97, A95, A98, FUNCT_1: 49;

          end;

        end;

      end;

      ( Sum ((1 / 2) GeoSeq )) = (1 / (1 - (1 / 2))) by A79, SERIES_1: 24;

      then

       A99: ( Sum (e (#) ((1 / 2) GeoSeq ))) = (e * 2) by A80, SERIES_1: 10;

      ( Sum me) <= ( Sum (e (#) ((1 / 2) GeoSeq ))) by A81, A47, SERIES_1: 20;

      then (M . MRHP) <= (2 * e) by A82, A99, XXREAL_0: 2;

      then

       A100: (M . (E \ F)) <= e0 by A75, XXREAL_0: 2;

      F c= L by A72, XBOOLE_1: 36;

      hence thesis by A19, A100, A91, XBOOLE_1: 1;

    end;