dualsp03.miz



    begin

    definition

      let X be non empty set;

      let F be sequence of ( Funcs ( NAT ,X));

      let k be Nat;

      :: original: .

      redefine

      func F . k -> sequence of X ;

      correctness

      proof

        ex f be Function st (F . k) = f & ( dom f) = NAT & ( rng f) c= X by FUNCT_2:def 2;

        hence thesis by FUNCT_2: 2;

      end;

    end

    theorem :: DUALSP03:1

    

     Lm73: for X be strict RealNormSpace, A be non empty Subset of X holds (for f be Point of ( DualSp X) st (for x be Point of X st x in A holds (( Bound2Lipschitz (f,X)) . x) = 0 ) holds ( Bound2Lipschitz (f,X)) = ( 0. ( DualSp X))) implies ( ClNLin A) = X

    proof

      let X be strict RealNormSpace, A be non empty Subset of X;

      assume

       A0: for f be Point of ( DualSp X) st (for x be Point of X st x in A holds (( Bound2Lipschitz (f,X)) . x) = 0 ) holds ( Bound2Lipschitz (f,X)) = ( 0. ( DualSp X));

      set M = ( ClNLin A);

      consider Z be Subset of X such that

       Q0: Z = the carrier of ( Lin A) & M = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),X)), ( Add_ (( Cl Z),X)), ( Mult_ (( Cl Z),X)), ( Norm_ (( Cl Z),X)) #) by NORMSP_3:def 20;

      reconsider Y = the carrier of M as non empty Subset of X by DUALSP01:def 16;

      

       Q23: Y is linearly-closed by NORMSP_3: 29;

      Y = the carrier of X

      proof

        assume Y <> the carrier of X;

        then not the carrier of X c= Y;

        then

        consider x0 be object such that

         Q25: x0 in the carrier of X & not x0 in Y;

        reconsider x0 as Point of X by Q25;

        consider G be Point of ( DualSp X) such that

         Q26: (for x be Point of X st x in Y holds (( Bound2Lipschitz (G,X)) . x) = 0 ) and

         Q27: (( Bound2Lipschitz (G,X)) . x0) = 1 by Q0, Q23, Q25, DUALSP02: 2;

        for x be Point of X st x in A holds (( Bound2Lipschitz (G,X)) . x) = 0

        proof

          let x be Point of X;

          assume x in A;

          then x in ( Lin A) by RLVECT_3: 15;

          then x in Y by Q0, NORMSP_3: 4, TARSKI:def 3;

          hence (( Bound2Lipschitz (G,X)) . x) = 0 by Q26;

        end;

        

        then (( Bound2Lipschitz (G,X)) . x0) = (( 0. ( DualSp X)) . x0) by A0

        .= ((the carrier of X --> 0 ) . x0) by DUALSP01: 25

        .= 0 ;

        hence contradiction by Q27;

      end;

      hence M = X by Q0, NORMSP_3: 26;

    end;

    theorem :: DUALSP03:2

    

     Th73: for X be strict RealNormSpace st ( DualSp X) is separable holds X is separable

    proof

      let X be strict RealNormSpace;

      set Y = ( DualSp X);

      assume Y is separable;

      then

      consider Yseq be sequence of Y such that

       P1: ( rng Yseq) is dense by NORMSP_3: 21;

      defpred P[ Nat, Point of X] means ( ||.(Yseq . $1).|| / 2) <= |.((Yseq . $1) . $2).| & ||.$2.|| <= 1;

      

       F2: for n be Element of NAT holds ex x be Point of X st P[n, x]

      proof

        let n be Element of NAT ;

        per cases ;

          suppose

           A1: ||.(Yseq . n).|| = 0 ;

          set x = ( 0. X);

          take x;

          thus ( ||.(Yseq . n).|| / 2) <= |.((Yseq . n) . x).| by A1, COMPLEX1: 46;

          thus ||.x.|| <= 1;

        end;

          suppose

           A21: ||.(Yseq . n).|| <> 0 ;

          assume

           A31: not (ex x be Point of X st ( ||.(Yseq . n).|| / 2) <= |.((Yseq . n) . x).| & ||.x.|| <= 1);

          reconsider f = (Yseq . n) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          now

            let r be Real;

            assume r in ( PreNorms f);

            then ex x be Point of X st r = |.(f . x).| & ||.x.|| <= 1;

            hence r <= ( ||.(Yseq . n).|| / 2) by A31;

          end;

          then ( upper_bound ( PreNorms f)) <= ( ||.(Yseq . n).|| / 2) by SEQ_4: 45;

          then ||.(Yseq . n).|| <= ( ||.(Yseq . n).|| / 2) by DUALSP01: 24;

          hence contradiction by XREAL_1: 216, A21;

        end;

      end;

      consider Xseq be Function of NAT , the carrier of X such that

       D4: for n be Element of NAT holds P[n, (Xseq . n)] from FUNCT_2:sch 3( F2);

      for n be Nat holds ( ||.(Yseq . n).|| / 2) <= |.((Yseq . n) . (Xseq . n)).| & ||.(Xseq . n).|| <= 1

      proof

        let n be Nat;

        n is Element of NAT by ORDINAL1:def 12;

        hence thesis by D4;

      end;

      then

      consider Xseq be sequence of X such that

       P2: for n be Nat holds ( ||.(Yseq . n).|| / 2) <= |.((Yseq . n) . (Xseq . n)).| & ||.(Xseq . n).|| <= 1;

      set X1 = ( rng Xseq);

      set M = ( ClNLin X1);

      set Y1 = ( rng Yseq);

      for f be Point of Y st (for x be Point of X st x in X1 holds (( Bound2Lipschitz (f,X)) . x) = 0 ) holds ( Bound2Lipschitz (f,X)) = ( 0. Y)

      proof

        let f be Point of Y;

        assume

         AS: for x be Point of X st x in X1 holds (( Bound2Lipschitz (f,X)) . x) = 0 ;

        reconsider f1 = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;

        

         A1: f1 = ( Bound2Lipschitz (f,X)) by DUALSP01: 23;

        consider seq be sequence of Y such that

         B0: ( rng seq) c= Y1 & seq is convergent & ( lim seq) = f by P1, NORMSP_3: 14;

        

         B1: ||.(seq - f).|| is convergent & ( lim ||.(seq - f).||) = 0 by B0, NORMSP_1: 24;

        

         B2: ||.seq.|| is convergent by B0, LOPBAN_1: 20;

        for n be Nat holds (((1 / 2) (#) ||.seq.||) . n) <= ( ||.(seq - f).|| . n)

        proof

          let n be Nat;

          (seq . n) in ( rng seq) by FUNCT_2: 4, ORDINAL1:def 12;

          then

          consider m be object such that

           E1: m in NAT & (Yseq . m) = (seq . n) by FUNCT_2: 11, B0;

          reconsider m as Nat by E1;

          reconsider x1 = (Xseq . m) as Point of X;

          

           C1: (f1 . x1) = 0 by A1, AS, E1, FUNCT_2: 4;

          

           C2: |.(((seq . n) . x1) - (f . x1)).| = |.(((seq . n) - f) . x1).| by DUALSP01: 33;

          reconsider g = ((seq . n) - f) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

           C3: |.(g . x1).| <= ( ||.((seq . n) - f).|| * ||.x1.||) by DUALSP01: 26;

          ( ||.((seq . n) - f).|| * ||.x1.||) <= ( ||.((seq . n) - f).|| * 1) by P2, XREAL_1: 64;

          then

           C4: |.(((seq . n) . x1) - (f . x1)).| <= ||.((seq . n) - f).|| by C2, C3, XXREAL_0: 2;

          ( ||.(seq . n).|| / 2) <= |.((seq . n) . x1).| by P2, E1;

          then

           C71: ((1 / 2) * ||.(seq . n).||) <= ||.((seq . n) - f).|| by C4, XXREAL_0: 2, C1;

          

           C8: ||.((seq . n) - f).|| = ||.((seq - f) . n).|| by NORMSP_1:def 4

          .= ( ||.(seq - f).|| . n) by NORMSP_0:def 4;

          ((1 / 2) * ( ||.seq.|| . n)) = (((1 / 2) (#) ||.seq.||) . n) by SEQ_1: 9;

          hence thesis by C71, NORMSP_0:def 4, C8;

        end;

        then

         B5: ( lim ((1 / 2) (#) ||.seq.||)) <= 0 by B1, B2, SEQ_2: 18;

        reconsider rseq = ||.seq.|| as Real_Sequence;

         B6:

        now

          let n be Nat;

           0 <= ((1 / 2) * ||.(seq . n).||);

          then 0 <= ((1 / 2) * (rseq . n)) by NORMSP_0:def 4;

          hence 0 <= (((1 / 2) (#) rseq) . n) by SEQ_1: 9;

        end;

        ((1 / 2) * ( lim rseq)) = ( lim ((1 / 2) (#) rseq)) by B0, LOPBAN_1: 20, SEQ_2: 8;

        then ( lim ||.seq.||) = 0 by B5, B6, B2, SEQ_2: 17;

        then ||.f.|| = 0 by B0, LOPBAN_1: 20;

        then f1 = ( 0. Y) by DUALSP01: 31;

        hence thesis by DUALSP01: 23;

      end;

      then M = X by Lm73;

      hence X is separable;

    end;

    theorem :: DUALSP03:3

    

     RNS3: for x be Real, x1 be Point of RNS_Real st x = x1 holds ( - x) = ( - x1)

    proof

      let x be Real, x1 be Point of RNS_Real ;

      assume

       AS: x = x1;

      reconsider mx = ( - x) as Point of RNS_Real by XREAL_0:def 1;

      (x1 + mx) = (x + ( - x)) by AS, BINOP_2:def 9;

      then (x1 + mx) = ( 0. RNS_Real );

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: DUALSP03:4

    

     RNS4: for x,y be Real, x1,y1 be Point of RNS_Real st x = x1 & y = y1 holds (x - y) = (x1 - y1)

    proof

      let x,y be Real, x1,y1 be Point of RNS_Real ;

      assume

       AS: x = x1 & y = y1;

      then

       P1: ( - y) = ( - y1) by RNS3;

      (x - y) = (x + ( - y));

      hence (x - y) = (x1 - y1) by AS, BINOP_2:def 9, P1;

    end;

    theorem :: DUALSP03:5

    

     RNS8: for seq be Real_Sequence, seq1 be sequence of RNS_Real st seq = seq1 holds seq is convergent iff seq1 is convergent

    proof

      let seq be Real_Sequence, seq1 be sequence of RNS_Real ;

      assume

       AS: seq = seq1;

      hereby

        assume

         P1: seq is convergent;

        reconsider s1 = ( lim seq) as Point of RNS_Real by XREAL_0:def 1;

        now

          let p be Real;

          assume 0 < p;

          then

          consider n be Nat such that

           P2: for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p by P1, SEQ_2:def 7;

          take n;

          hereby

            let m be Nat;

            assume n <= m;

            then

             P3: |.((seq . m) - ( lim seq)).| < p by P2;

            ((seq . m) - ( lim seq)) = ((seq1 . m) - s1) by AS, RNS4;

            hence ||.((seq1 . m) - s1).|| < p by P3, EUCLID:def 2;

          end;

        end;

        hence seq1 is convergent;

      end;

      assume

       P4: seq1 is convergent;

      reconsider s1 = ( lim seq1) as Real;

      now

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

         P2: for m be Nat st n <= m holds ||.((seq1 . m) - ( lim seq1)).|| < p by P4, NORMSP_1:def 7;

        take n;

        hereby

          let m be Nat;

          assume n <= m;

          then

           P3: ||.((seq1 . m) - ( lim seq1)).|| < p by P2;

          ((seq1 . m) - ( lim seq1)) = ((seq . m) - s1) by AS, RNS4;

          hence |.((seq . m) - s1).| < p by P3, EUCLID:def 2;

        end;

      end;

      hence seq is convergent;

    end;

    theorem :: DUALSP03:6

    

     RNS9: for seq be Real_Sequence, seq1 be sequence of RNS_Real st seq = seq1 & seq is convergent holds ( lim seq) = ( lim seq1)

    proof

      let seq be Real_Sequence, seq1 be sequence of RNS_Real ;

      assume

       AS: seq = seq1;

      assume

       P1: seq is convergent;

      then

       P5: seq1 is convergent by AS, RNS8;

      reconsider s1 = ( lim seq) as Point of RNS_Real by XREAL_0:def 1;

      now

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

         P2: for m be Nat st n <= m holds |.((seq . m) - ( lim seq)).| < p by P1, SEQ_2:def 7;

        take n;

        hereby

          let m be Nat;

          assume n <= m;

          then

           P3: |.((seq . m) - ( lim seq)).| < p by P2;

          ((seq . m) - ( lim seq)) = ((seq1 . m) - s1) by AS, RNS4;

          hence ||.((seq1 . m) - s1).|| < p by P3, EUCLID:def 2;

        end;

      end;

      hence ( lim seq1) = ( lim seq) by P5, NORMSP_1:def 7;

    end;

    theorem :: DUALSP03:7

    

     RNS11: for seq1 be sequence of RNS_Real st seq1 is Cauchy_sequence_by_Norm holds seq1 is convergent

    proof

      let seq1 be sequence of RNS_Real ;

      assume

       AS: seq1 is Cauchy_sequence_by_Norm;

      reconsider seq = seq1 as Real_Sequence;

      for s be Real st 0 < s holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - (seq . n)).| < s

      proof

        let s be Real;

        assume 0 < s;

        then

        consider k be Nat such that

         P1: for n,m be Nat st n >= k & m >= k holds ||.((seq1 . n) - (seq1 . m)).|| < s by AS, RSSPACE3: 8;

        take k;

        hereby

          let m be Nat;

          assume k <= m;

          then

           P2: ||.((seq1 . m) - (seq1 . k)).|| < s by P1;

          ((seq1 . m) - (seq1 . k)) = ((seq . m) - (seq . k)) by RNS4;

          hence |.((seq . m) - (seq . k)).| < s by EUCLID:def 2, P2;

        end;

      end;

      then seq is convergent by SEQ_4: 41;

      hence thesis by RNS8;

    end;

    registration

      cluster RNS_Real -> complete;

      correctness by LOPBAN_1:def 15, RNS11;

    end

    definition

      let X be RealNormSpace, g be sequence of ( DualSp X), x be Point of X;

      :: DUALSP03:def1

      func g # x -> Real_Sequence means

      : Def1: for i be Nat holds (it . i) = ((g . i) . x);

      existence

      proof

        deffunc F( Element of NAT ) = ((g . $1) . x);

        consider f be Real_Sequence such that

         A1: for i be Element of NAT holds (f . i) = F(i) from FUNCT_2:sch 4;

        take f;

        hereby

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          hence (f . i) = ((g . i) . x) by A1;

        end;

      end;

      uniqueness

      proof

        let p1,p2 be Real_Sequence;

        assume

         B1: (for i be Nat holds (p1 . i) = ((g . i) . x)) & (for i be Nat holds (p2 . i) = ((g . i) . x));

        

         B2: ( dom p1) = NAT & ( dom p2) = NAT by FUNCT_2:def 1;

        now

          let i be object;

          assume i in ( dom p1);

          then

          reconsider i1 = i as Nat;

          (p1 . i) = ((g . i1) . x) by B1;

          hence (p1 . i) = (p2 . i) by B1;

        end;

        hence p1 = p2 by B2;

      end;

    end

    begin

    definition

      let X be RealNormSpace, x be sequence of X;

      :: DUALSP03:def2

      attr x is weakly-convergent means ex x0 be Point of X st for f be Lipschitzian linear-Functional of X holds (f * x) is convergent & ( lim (f * x)) = (f . x0);

    end

    theorem :: DUALSP03:8

    

     WEAKLM1: for X be RealNormSpace, x be sequence of X st ( rng x) c= {( 0. X)} holds x is weakly-convergent

    proof

      let X be RealNormSpace, x be sequence of X;

      assume

       AS: ( rng x) c= {( 0. X)};

      reconsider x0 = ( 0. X) as Point of X;

      for f be Lipschitzian linear-Functional of X holds (f * x) is convergent & ( lim (f * x)) = (f . x0)

      proof

        let f be Lipschitzian linear-Functional of X;

        

         A2: for p be Real, n be Nat st 0 < p holds |.(((f * x) . n) - (f . x0)).| < p

        proof

          let p be Real, n be Nat;

          assume

           AS1: 0 < p;

          

           C21: (x . n) in ( rng x) by FUNCT_2: 4, ORDINAL1:def 12;

          ((f * x) . n) = (f . (x . n)) by ORDINAL1:def 12, FUNCT_2: 15;

          then ((f * x) . n) = (f . ( 0. X)) by TARSKI:def 1, AS, C21;

          hence |.(((f * x) . n) - (f . x0)).| < p by AS1, COMPLEX1: 44;

        end;

        

         A1: for p be Real st 0 < p holds ex m be Nat st for n be Nat st m <= n holds |.(((f * x) . n) - (f . x0)).| < p

        proof

          let p be Real;

          assume

           AS1: 0 < p;

          take m = 0 ;

          thus thesis by AS1, A2;

        end;

        then (f * x) is convergent;

        hence thesis by A1, SEQ_2:def 7;

      end;

      hence x is weakly-convergent;

    end;

    definition

      let X be RealNormSpace, x be sequence of X;

      assume

       A1: x is weakly-convergent;

      :: DUALSP03:def3

      func w-lim x -> Point of X means

      : DefWeaklim: for f be Lipschitzian linear-Functional of X holds (f * x) is convergent & ( lim (f * x)) = (f . it );

      existence by A1;

      uniqueness

      proof

        given g1,g2 be Point of X such that

         A2: for f be Lipschitzian linear-Functional of X holds (f * x) is convergent & ( lim (f * x)) = (f . g1) and

         A3: for f be Lipschitzian linear-Functional of X holds (f * x) is convergent & ( lim (f * x)) = (f . g2) and

         A4: g1 <> g2;

        now

          let f be Lipschitzian linear-Functional of X;

          (f . (g1 - g2)) = ((f . g1) - (f . g2)) by HAHNBAN: 19

          .= (( lim (f * x)) - (f . g2)) by A2

          .= (( lim (f * x)) - ( lim (f * x))) by A3;

          hence (f . (g1 - g2)) = 0 ;

        end;

        then (g1 - g2) = ( 0. X) by DUALSP02: 8;

        hence contradiction by A4, RLVECT_1: 21;

      end;

    end

    theorem :: DUALSP03:9

    for X be RealNormSpace, x be sequence of X st x is convergent holds x is weakly-convergent & ( w-lim x) = ( lim x)

    proof

      let X be RealNormSpace, x be sequence of X such that

       A2: x is convergent;

      reconsider x0 = ( lim x) as Point of X;

      

       A3: for f be Lipschitzian linear-Functional of X holds (f * x) is convergent & ( lim (f * x)) = (f . x0)

      proof

        let f be Lipschitzian linear-Functional of X;

        

         B1: ( dom f) = the carrier of X by FUNCT_2:def 1;

        consider K be Real such that

         B3: 0 <= K & for x be VECTOR of X holds |.(f . x).| <= (K * ||.x.||) by DUALSP01:def 9;

        for x1,x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds |.((f /. x1) - (f /. x2)).| <= ((K + 1) * ||.(x1 - x2).||)

        proof

          let x1,x2 be Point of X;

          assume x1 in the carrier of X & x2 in the carrier of X;

          

           C2: |.((f /. x1) - (f /. x2)).| = |.(f . (x1 - x2)).| by HAHNBAN: 19;

          

           C3: |.(f . (x1 - x2)).| <= (K * ||.(x1 - x2).||) by B3;

          ( 0 + K) <= (K + 1) by XREAL_1: 8;

          then (K * ||.(x1 - x2).||) <= ((K + 1) * ||.(x1 - x2).||) by XREAL_1: 64;

          hence thesis by XXREAL_0: 2, C2, C3;

        end;

        then f is_Lipschitzian_on the carrier of X by FUNCT_2:def 1, B3;

        then f is_continuous_on the carrier of X by NFCONT_1: 46;

        then

         B81: f is_continuous_in x0;

        

         B6: ( rng x) c= the carrier of X;

        then (f /* x) = (f * x) by B1, FUNCT_2:def 11;

        hence (f * x) is convergent & ( lim (f * x)) = (f . x0) by B81, A2, B1, B6;

      end;

      then

       A4: x is weakly-convergent;

      now

        let f be Lipschitzian linear-Functional of X;

        (f . (( w-lim x) - x0)) = ((f . ( w-lim x)) - (f . x0)) by HAHNBAN: 19

        .= (( lim (f * x)) - (f . x0)) by A4, DefWeaklim

        .= (( lim (f * x)) - ( lim (f * x))) by A3;

        hence (f . (( w-lim x) - x0)) = 0 ;

      end;

      then (( w-lim x) - ( lim x)) = ( 0. X) by DUALSP02: 8;

      hence thesis by A3, RLVECT_1: 21;

    end;

    theorem :: DUALSP03:10

    

     Th79: for X be RealNormSpace, x be sequence of X st X is non trivial & x is weakly-convergent holds ||.x.|| is bounded & ||.( w-lim x).|| <= ( lim_inf ||.x.||) & ( w-lim x) in ( ClNLin ( rng x))

    proof

      let X be RealNormSpace, x be sequence of X;

      assume

       AS: X is non trivial & x is weakly-convergent;

      reconsider x0 = ( w-lim x) as Point of X;

      for f be Point of ( DualSp X) holds ex Kf be Real st 0 <= Kf & for y be Point of X st y in ( rng x) holds |.(f . y).| <= Kf

      proof

        let f be Point of ( DualSp X);

        reconsider h = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;

        (h * x) is convergent by AS;

        then

        consider Kf be Real such that

         A1: 0 < Kf & for n be Nat holds |.((h * x) . n).| < Kf by SEQ_2: 3;

        for y be Point of X st y in ( rng x) holds |.(f . y).| <= Kf

        proof

          let y be Point of X;

          assume y in ( rng x);

          then

          consider m be Nat such that

           A2: y = (x . m) by NFCONT_1: 6;

           |.((h * x) . m).| = |.(f . (x . m)).| by FUNCT_2: 15, ORDINAL1:def 12;

          hence thesis by A2, A1;

        end;

        hence thesis by A1;

      end;

      then

      consider K be Real such that

       A4: 0 <= K & for y be Point of X st y in ( rng x) holds ||.y.|| <= K by AS, DUALSP02: 19;

      

       A5: for n be Nat holds ( ||.x.|| . n) <= K

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then ||.(x . n).|| <= K by A4, FUNCT_2: 4;

        hence thesis by NORMSP_0:def 4;

      end;

      

       A6: (K + 0 ) < (K + 1) by XREAL_1: 8;

      

       X10: for n be Nat holds |.( ||.x.|| . n).| < (K + 1)

      proof

        let n be Nat;

        ( ||.x.|| . n) <= K by A5;

        then

         A7: ( ||.x.|| . n) < (K + 1) by A6, XXREAL_0: 2;

         0 <= ||.(x . n).||;

        then 0 <= ( ||.x.|| . n) by NORMSP_0:def 4;

        hence thesis by A7, ABSVALUE:def 1;

      end;

      then

       X1: ||.x.|| is bounded by A4, SEQ_2: 3;

      

       B0: for f be Point of ( DualSp X) holds |.(f . x0).| <= (( lim_inf ||.x.||) * ||.f.||)

      proof

        let f be Point of ( DualSp X);

        reconsider h = f as Lipschitzian linear-Functional of X by DUALSP01:def 10;

        

         B1: (h * x) is convergent & ( lim (h * x)) = (h . x0) by DefWeaklim, AS;

        

         B6: for n be Nat holds ( |.(h * x).| . n) <= (( ||.f.|| (#) ||.x.||) . n)

        proof

          let n be Nat;

          

           D21: |.(h . (x . n)).| <= ( ||.f.|| * ||.(x . n).||) by DUALSP01: 26;

           |.(h . (x . n)).| = |.((h * x) . n).| by FUNCT_2: 15, ORDINAL1:def 12;

          then |.((h * x) . n).| <= ( ||.f.|| * ( ||.x.|| . n)) by D21, NORMSP_0:def 4;

          then ( |.(h * x).| . n) <= ( ||.f.|| * ( ||.x.|| . n)) by SEQ_1: 12;

          hence thesis by SEQ_1: 9;

        end;

        ( ||.f.|| (#) ||.x.||) is bounded by A4, SEQ_2: 3, X10, SEQM_3: 37;

        then ( lim_inf |.(h * x).|) <= ( lim_inf ( ||.f.|| (#) ||.x.||)) by B1, B6, RINFSUP1: 91;

        then

         B7: ( lim |.(h * x).|) <= ( lim_inf ( ||.f.|| (#) ||.x.||)) by B1, RINFSUP1: 89;

        ( lim_inf ( ||.f.|| (#) ||.x.||)) = (( lim_inf ||.x.||) * ||.f.||) by X1, LOPBAN_5: 1;

        hence thesis by SEQ_4: 14, B1, B7;

      end;

      now

        let s be Real;

        assume

         D5: 0 < s;

        for k be Nat holds ( 0 - s) < ( ||.x.|| . ( 0 + k))

        proof

          let k be Nat;

           ||.(x . k).|| = ( ||.x.|| . k) by NORMSP_0:def 4;

          hence thesis by D5;

        end;

        hence ex n be Nat st for k be Nat holds ( 0 - s) < ( ||.x.|| . (n + k));

      end;

      then

       B8: 0 <= ( lim_inf ||.x.||) by X1, RINFSUP1: 82;

      consider Y be non empty Subset of REAL such that

       B9: Y = { |.(( Bound2Lipschitz (F,X)) . x0).| where F be Point of ( DualSp X) : ||.F.|| <= 1 } & ||.x0.|| = ( upper_bound Y) by AS, DUALSP02: 7;

       X21:

      now

        let r be Real;

        assume r in Y;

        then

        consider F be Point of ( DualSp X) such that

         D7: r = |.(( Bound2Lipschitz (F,X)) . x0).| & ||.F.|| <= 1 by B9;

        reconsider f1 = F as Lipschitzian linear-Functional of X by DUALSP01:def 10;

        

         D8: f1 = ( Bound2Lipschitz (F,X)) by DUALSP01: 23;

        

         D9: |.(F . x0).| <= (( lim_inf ||.x.||) * ||.F.||) by B0;

        (( lim_inf ||.x.||) * ||.F.||) <= (( lim_inf ||.x.||) * 1) by B8, D7, XREAL_1: 64;

        hence r <= ( lim_inf ||.x.||) by D7, D8, D9, XXREAL_0: 2;

      end;

      x0 in ( ClNLin ( rng x))

      proof

        set M = ( ClNLin ( rng x));

        consider Z be Subset of X such that

         C1: Z = the carrier of ( Lin ( rng x)) & M = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),X)), ( Add_ (( Cl Z),X)), ( Mult_ (( Cl Z),X)), ( Norm_ (( Cl Z),X)) #) by NORMSP_3:def 20;

        reconsider Y = the carrier of M as Subset of X by DUALSP01:def 16;

        

         C3: Y is linearly-closed by NORMSP_3: 29;

        x0 in Y

        proof

          assume

           AS0: not x0 in Y;

          consider G be Point of ( DualSp X) such that

           C5: (for y be Point of X st y in Y holds (( Bound2Lipschitz (G,X)) . y) = 0 ) and

           C6: (( Bound2Lipschitz (G,X)) . x0) = 1 by C1, C3, AS0, DUALSP02: 2;

          reconsider g = G as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

           C7: g = ( Bound2Lipschitz (G,X)) by DUALSP01: 23;

          

           C8: (g * x) is convergent by AS;

          

           C101: for n be Nat holds ((g * x) . n) <= (( seq_const 0 ) . n)

          proof

            let n be Nat;

            n in NAT by ORDINAL1:def 12;

            then (x . n) in ( Lin ( rng x)) by RLVECT_3: 15, FUNCT_2: 4;

            then (x . n) in Y by C1, NORMSP_3: 4, TARSKI:def 3;

            then (g . (x . n)) = 0 by C5, C7;

            then ((g * x) . n) = 0 by FUNCT_2: 15, ORDINAL1:def 12;

            hence thesis;

          end;

          

           C111: ( lim ( seq_const 0 )) = (( seq_const 0 ) . 0 ) by SEQ_4: 26

          .= 0 ;

          ( lim (g * x)) = (g . x0) by DefWeaklim, AS

          .= 1 by C6, DUALSP01: 23;

          hence contradiction by C111, C101, C8, SEQ_2: 18;

        end;

        hence x0 in M;

      end;

      hence thesis by A4, SEQ_2: 3, X10, B9, SEQ_4: 45, X21;

    end;

    definition

      let X be RealNormSpace, g be sequence of ( DualSp X);

      :: DUALSP03:def4

      attr g is weakly*-convergent means ex g0 be Point of ( DualSp X) st for x be Point of X holds (g # x) is convergent & ( lim (g # x)) = (g0 . x);

    end

    definition

      let X be RealNormSpace, g be sequence of ( DualSp X);

      assume

       A1: g is weakly*-convergent;

      :: DUALSP03:def5

      func w*-lim g -> Point of ( DualSp X) means

      : Def2: for x be Point of X holds (g # x) is convergent & ( lim (g # x)) = (it . x);

      existence by A1;

      uniqueness

      proof

        let f1,f2 be Point of ( DualSp X);

        assume

         B1: (for x be Point of X holds (g # x) is convergent & ( lim (g # x)) = (f1 . x)) & (for x be Point of X holds (g # x) is convergent & ( lim (g # x)) = (f2 . x));

        

         B2: f1 is Lipschitzian linear-Functional of X & f2 is Lipschitzian linear-Functional of X by DUALSP01:def 10;

        for x be Point of X holds (f1 . x) = (f2 . x)

        proof

          let x be Point of X;

          

          thus (f1 . x) = ( lim (g # x)) by B1

          .= (f2 . x) by B1;

        end;

        hence f1 = f2 by B2, FUNCT_2:def 8;

      end;

    end

    theorem :: DUALSP03:11

    for X be RealNormSpace, g be sequence of ( DualSp X) st g is convergent holds g is weakly*-convergent & ( w*-lim g) = ( lim g)

    proof

      let X be RealNormSpace, g be sequence of ( DualSp X) such that

       A2: g is convergent;

      reconsider g0 = ( lim g) as Point of ( DualSp X);

      

       A3: for x be Point of X holds (g # x) is convergent & ( lim (g # x)) = (g0 . x)

      proof

        let x be Point of X;

        

         B2: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds |.(((g # x) . n) - (g0 . x)).| < r

        proof

          let r be Real;

          set p = (r / ( ||.x.|| + 1));

          assume

           C00: 0 < r;

          then

          consider m be Nat such that

           C1: for n be Nat st m <= n holds ||.((g . n) - g0).|| < p by A2, NORMSP_1:def 7;

          (p * ( ||.x.|| + 1)) = r by XCMPLX_1: 87;

          then

           C0: 0 < p & (p * ||.x.||) < r by C00, XREAL_1: 29, XREAL_1: 68;

          

           CX: for n be Nat st m <= n holds |.(((g # x) . n) - (g0 . x)).| < r

          proof

            let n be Nat;

            assume m <= n;

            then ||.((g . n) - g0).|| < p by C1;

            then

             D4: ( ||.((g . n) - g0).|| * ||.x.||) <= (p * ||.x.||) by XREAL_1: 64;

            

             D2: |.(((g # x) . n) - (g0 . x)).| = |.(((g . n) . x) - (g0 . x)).| by Def1

            .= |.(((g . n) - g0) . x).| by DUALSP01: 33;

            reconsider h = ((g . n) - g0) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

             |.(h . x).| <= ( ||.((g . n) - g0).|| * ||.x.||) by DUALSP01: 26;

            then |.(h . x).| <= (p * ||.x.||) by D4, XXREAL_0: 2;

            hence thesis by D2, C0, XXREAL_0: 2;

          end;

          take m;

          thus thesis by CX;

        end;

        then (g # x) is convergent;

        hence thesis by B2, SEQ_2:def 7;

      end;

      then g is weakly*-convergent;

      hence thesis by A3, Def2;

    end;

    theorem :: DUALSP03:12

    

     Lm710A: for X be RealNormSpace, f be sequence of ( DualSp X) st f is weakly-convergent holds f is weakly*-convergent

    proof

      let X be RealNormSpace, f be sequence of ( DualSp X);

      assume

       AS: f is weakly-convergent;

      reconsider f0 = ( w-lim f) as Point of ( DualSp X);

      for x be Point of X holds (f # x) is convergent & ( lim (f # x)) = (f0 . x)

      proof

        let x be Point of X;

        reconsider G = ( BiDual x) as Lipschitzian linear-Functional of ( DualSp X) by DUALSP01:def 10;

        

         C3: (G * f) is convergent & ( lim (G * f)) = (G . f0) by DefWeaklim, AS;

        

         B4: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds |.(((f # x) . n) - (f0 . x)).| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

           C1: for n be Nat st m <= n holds |.(((G * f) . n) - (G . f0)).| < r by C3, SEQ_2:def 7;

          take m;

          thus for n be Nat st m <= n holds |.(((f # x) . n) - (f0 . x)).| < r

          proof

            let n be Nat;

            assume

             D3: m <= n;

            

             B1: (G . f0) = (f0 . x) by DUALSP02:def 1;

            ((G * f) . n) = (G . (f . n)) by FUNCT_2: 15, ORDINAL1:def 12

            .= ((f . n) . x) by DUALSP02:def 1;

            then ((G * f) . n) = ((f # x) . n) by Def1;

            hence thesis by B1, C1, D3;

          end;

        end;

        then (f # x) is convergent;

        hence thesis by B4, SEQ_2:def 7;

      end;

      hence f is weakly*-convergent;

    end;

    theorem :: DUALSP03:13

    for X be RealNormSpace, f be sequence of ( DualSp X) st X is Reflexive holds f is weakly-convergent iff f is weakly*-convergent

    proof

      let X be RealNormSpace, f be sequence of ( DualSp X);

      assume

       AS: X is Reflexive;

      thus f is weakly-convergent implies f is weakly*-convergent by Lm710A;

      thus f is weakly*-convergent implies f is weakly-convergent

      proof

        assume

         AS1: f is weakly*-convergent;

        reconsider f0 = ( w*-lim f) as Point of ( DualSp X);

        for F be Lipschitzian linear-Functional of ( DualSp X) holds (F * f) is convergent & ( lim (F * f)) = (F . f0)

        proof

          let F be Lipschitzian linear-Functional of ( DualSp X);

          reconsider G = F as Point of ( DualSp ( DualSp X)) by DUALSP01:def 10;

          consider x be Point of X such that

           B1: for f be Point of ( DualSp X) holds (G . f) = (f . x) by AS, DUALSP02: 21;

          

           C4: (f # x) is convergent & ( lim (f # x)) = (f0 . x) by AS1, Def2;

          

           B5: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds |.(((F * f) . n) - (F . f0)).| < r

          proof

            let r be Real;

            assume 0 < r;

            then

            consider m be Nat such that

             C1: for n be Nat st m <= n holds |.(((f # x) . n) - (f0 . x)).| < r by C4, SEQ_2:def 7;

            take m;

            hereby

              let n be Nat;

              assume

               D3: m <= n;

              ((F * f) . n) = (G . (f . n)) by FUNCT_2: 15, ORDINAL1:def 12;

              then ((F * f) . n) = ((f . n) . x) by B1;

              then ((F * f) . n) = ((f # x) . n) by Def1;

              then |.(((F * f) . n) - (F . f0)).| = |.(((f # x) . n) - (f0 . x)).| by B1;

              hence |.(((F * f) . n) - (F . f0)).| < r by C1, D3;

            end;

          end;

          then (F * f) is convergent;

          hence thesis by B5, SEQ_2:def 7;

        end;

        hence f is weakly-convergent;

      end;

    end;

    theorem :: DUALSP03:14

    

     Lm55: for X be RealBanachSpace, T be Subset of ( DualSp X) st (for x be Point of X holds ex K be Real st 0 <= K & for f be Point of ( DualSp X) st f in T holds |.(f . x).| <= K) holds ex L be Real st 0 <= L & for f be Point of ( DualSp X) st f in T holds ||.f.|| <= L

    proof

      let X be RealBanachSpace, T be Subset of ( DualSp X);

      assume

       AS: for x be Point of X holds ex K be Real st 0 <= K & for f be Point of ( DualSp X) st f in T holds |.(f . x).| <= K;

      reconsider T1 = T as Subset of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) by DUALSP02: 14;

      for x be Point of X holds ex K be Real st 0 <= K & for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) st f in T1 holds ||.(f . x).|| <= K

      proof

        let x be Point of X;

        consider K be Real such that

         B1: 0 <= K & for f be Point of ( DualSp X) st f in T holds |.(f . x).| <= K by AS;

        take K;

        for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) st f in T1 holds ||.(f . x).|| <= K

        proof

          let f be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

          assume

           C2: f in T1;

          then

          reconsider f1 = f as Point of ( DualSp X);

           |.(f1 . x).| = ||.(f . x).|| by EUCLID:def 2;

          hence thesis by C2, B1;

        end;

        hence thesis by B1;

      end;

      then

      consider L be Real such that

       A1: 0 <= L & for f be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) st f in T1 holds ||.f.|| <= L by LOPBAN_5: 5;

      take L;

      for f be Point of ( DualSp X) st f in T holds ||.f.|| <= L

      proof

        let f be Point of ( DualSp X);

        assume

         C5: f in T;

        then f in T1;

        then

        reconsider f1 = f as Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

         ||.f1.|| = ||.f.|| by DUALSP02: 18;

        hence thesis by C5, A1;

      end;

      hence thesis by A1;

    end;

    theorem :: DUALSP03:15

    

     Th711: for X be RealBanachSpace, f be sequence of ( DualSp X) st f is weakly*-convergent holds ||.f.|| is bounded & ||.( w*-lim f).|| <= ( lim_inf ||.f.||)

    proof

      let X be RealBanachSpace, f be sequence of ( DualSp X);

      assume

       AS: f is weakly*-convergent;

      reconsider f0 = ( w*-lim f) as Point of ( DualSp X);

      for x be Point of X holds ex K be Real st 0 <= K & for g be Point of ( DualSp X) st g in ( rng f) holds |.(g . x).| <= K

      proof

        let x be Point of X;

        (f # x) is convergent by AS;

        then

        consider K be Real such that

         A2: for n be Nat holds ( |.(f # x).| . n) < K by SEQ_2:def 3;

        

         A3: for g be Point of ( DualSp X) st g in ( rng f) holds |.(g . x).| <= K

        proof

          let g be Point of ( DualSp X);

          assume g in ( rng f);

          then

          consider n be object such that

           A4: n in NAT & g = (f . n) by FUNCT_2: 11;

          reconsider n as Nat by A4;

          ((f . n) . x) = ((f # x) . n) by Def1;

          then |.(g . x).| = ( |.(f # x).| . n) by A4, SEQ_1: 12;

          hence thesis by A2;

        end;

        

         B6: ( |.(f # x).| . 0 ) < K by A2;

         0 <= |.((f # x) . 0 ).| by COMPLEX1: 46;

        then 0 <= K by B6, SEQ_1: 12;

        hence thesis by A3;

      end;

      then

      consider L be Real such that

       A7: 0 <= L and

       A8: for g be Point of ( DualSp X) st g in ( rng f) holds ||.g.|| <= L by Lm55;

      

       Y1: for n be Nat holds |.( ||.f.|| . n).| < (L + 1)

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then ||.(f . n).|| <= L by A8, FUNCT_2: 4;

        then ||.(f . n).|| < (L + 1) by XREAL_1: 39;

        then |. ||.(f . n).||.| < (L + 1) by ABSVALUE:def 1;

        hence thesis by NORMSP_0:def 4;

      end;

      then

       X1: ||.f.|| is bounded by A7, SEQ_2: 3;

      

       B1: for x be Point of X holds |.(f0 . x).| <= (( lim_inf ||.f.||) * ||.x.||)

      proof

        let x be Point of X;

        

         B3: for n be Nat holds ( |.(f # x).| . n) <= (( ||.x.|| (#) ||.f.||) . n)

        proof

          let n be Nat;

          reconsider h = (f . n) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

           B4: ( |.(f # x).| . n) = |.((f # x) . n).| by SEQ_1: 12;

           ||.(f . n).|| = ( ||.f.|| . n) by NORMSP_0:def 4;

          then ( ||.(f . n).|| * ||.x.||) = (( ||.x.|| (#) ||.f.||) . n) by SEQ_1: 9;

          then |.(h . x).| <= (( ||.x.|| (#) ||.f.||) . n) by DUALSP01: 26;

          hence thesis by B4, Def1;

        end;

        

         B6: ( lim_inf ( ||.x.|| (#) ||.f.||)) = (( lim_inf ||.f.||) * ||.x.||) by X1, LOPBAN_5: 1;

        

         B7: (f # x) is convergent & ( lim (f # x)) = (f0 . x) by AS, Def2;

        ( ||.x.|| (#) ||.f.||) is bounded by A7, SEQ_2: 3, Y1, SEQM_3: 37;

        then

         B9: ( lim_inf |.(f # x).|) <= ( lim_inf ( ||.x.|| (#) ||.f.||)) by B3, RINFSUP1: 91, B7;

        ( lim |.(f # x).|) = |.(f0 . x).| by B7, SEQ_4: 14;

        hence thesis by B6, B7, RINFSUP1: 89, B9;

      end;

      now

        let s be Real;

        assume

         B9: 0 < s;

        for k be Nat holds ( 0 - s) < ( ||.f.|| . ( 0 + k))

        proof

          let k be Nat;

           ||.(f . k).|| = ( ||.f.|| . k) by NORMSP_0:def 4;

          hence thesis by B9;

        end;

        hence ex n be Nat st for k be Nat holds ( 0 - s) < ( ||.f.|| . (n + k));

      end;

      then

       B10: 0 <= ( lim_inf ||.f.||) by X1, RINFSUP1: 82;

      reconsider g = f0 as Lipschitzian linear-Functional of X by DUALSP01:def 10;

      now

        let k be Real;

        assume k in ( PreNorms g);

        then

        consider x be Point of X such that

         B11: k = |.(g . x).| & ||.x.|| <= 1;

        

         B12: |.(f0 . x).| <= (( lim_inf ||.f.||) * ||.x.||) by B1;

        (( lim_inf ||.f.||) * ||.x.||) <= (( lim_inf ||.f.||) * 1) by B10, B11, XREAL_1: 64;

        hence k <= ( lim_inf ||.f.||) by B11, B12, XXREAL_0: 2;

      end;

      then ( upper_bound ( PreNorms g)) <= ( lim_inf ||.f.||) by SEQ_4: 45;

      hence thesis by A7, SEQ_2: 3, Y1, DUALSP01: 24;

    end;

    theorem :: DUALSP03:16

    

     RNSBH1: for X be RealNormSpace, x be Point of X, vseq be sequence of ( DualSp X), vseq1 be sequence of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) st vseq = vseq1 holds (vseq # x) = (vseq1 # x)

    proof

      let X be RealNormSpace, x be Point of X, vseq be sequence of ( DualSp X), vseq1 be sequence of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

      assume

       AS: vseq = vseq1;

      for n be Element of NAT holds ((vseq # x) . n) = ((vseq1 # x) . n)

      proof

        let n be Element of NAT ;

        ((vseq # x) . n) = ((vseq . n) . x) by Def1;

        hence ((vseq # x) . n) = ((vseq1 # x) . n) by AS, LOPBAN_5:def 2;

      end;

      hence thesis;

    end;

    theorem :: DUALSP03:17

    

     Th712A: for X be RealBanachSpace, X0 be Subset of X, vseq be sequence of ( DualSp X) st ||.vseq.|| is bounded & X0 is dense & (for x be Point of X st x in X0 holds (vseq # x) is convergent) holds vseq is weakly*-convergent

    proof

      let X be RealBanachSpace, X0 be Subset of X, vseq be sequence of ( DualSp X);

      assume that

       A1: ||.vseq.|| is bounded and

       A2: X0 is dense and

       A3: for x be Point of X st x in X0 holds (vseq # x) is convergent;

      reconsider vseq1 = vseq as sequence of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) by DUALSP02: 14;

      reconsider X01 = X0 as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      

       B1: for x be Point of X st x in X01 holds (vseq1 # x) is convergent

      proof

        let x be Point of X;

        assume x in X01;

        then

         B11: (vseq # x) is convergent by A3;

        (vseq1 # x) = (vseq # x) by RNSBH1;

        hence (vseq1 # x) is convergent by RNS8, B11;

      end;

      

       B2: for x be Point of X holds ex K be Real st 0 <= K & for n be Nat holds ||.((vseq1 # x) . n).|| <= K

      proof

        let x be Point of X;

        consider K0 be Real such that

         B20: 0 < K0 & for n be Nat holds |.( ||.vseq.|| . n).| < K0 by A1, SEQ_2: 3;

        reconsider K = ((K0 * ||.x.||) + 1) as Real;

        take K;

        

         C0: ((K0 * ||.x.||) + 0 ) < ((K0 * ||.x.||) + 1) by XREAL_1: 8;

        thus 0 <= K by B20;

        thus for n be Nat holds ||.((vseq1 # x) . n).|| <= K

        proof

          let n be Nat;

           |.( ||.vseq.|| . n).| < K0 by B20;

          then |. ||.(vseq . n).||.| < K0 by NORMSP_0:def 4;

          then

           A5: ||.(vseq . n).|| < K0 by ABSVALUE:def 1;

          reconsider h = (vseq . n) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

           B1: |.(h . x).| <= ( ||.(vseq . n).|| * ||.x.||) by DUALSP01: 26;

          

           C3: ( ||.(vseq . n).|| * ||.x.||) <= (K0 * ||.x.||) by A5, XREAL_1: 64;

           |.((vseq # x) . n).| = |.((vseq . n) . x).| by Def1;

          then |.((vseq # x) . n).| <= (K0 * ||.x.||) by C3, B1, XXREAL_0: 2;

          then

           B4: |.((vseq # x) . n).| <= K by C0, XXREAL_0: 2;

          (vseq # x) = (vseq1 # x) by RNSBH1;

          hence ||.((vseq1 # x) . n).|| <= K by B4, EUCLID:def 2;

        end;

      end;

      X01 is dense by A2, NORMSP_3: 15;

      then

      consider tseq be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) such that

       B4: (for x be Point of X holds (vseq1 # x) is convergent & (tseq . x) = ( lim (vseq1 # x)) & ||.(tseq . x).|| <= (( lim_inf ||.vseq1.||) * ||.x.||)) & ||.tseq.|| <= ( lim_inf ||.vseq1.||) by B1, B2, LOPBAN_5: 8;

      reconsider g0 = tseq as Point of ( DualSp X) by DUALSP02: 14;

      for x be Point of X holds (vseq # x) is convergent & ( lim (vseq # x)) = (g0 . x)

      proof

        let x be Point of X;

        

         B7: (vseq1 # x) = (vseq # x) by RNSBH1;

        (vseq1 # x) is convergent & (tseq . x) = ( lim (vseq1 # x)) by B4;

        hence (vseq # x) is convergent by B7, RNS8;

        then ( lim (vseq # x)) = ( lim (vseq1 # x)) by RNSBH1, RNS9;

        hence (g0 . x) = ( lim (vseq # x)) by B4;

      end;

      hence vseq is weakly*-convergent;

    end;

    theorem :: DUALSP03:18

    for X be RealBanachSpace, f be sequence of ( DualSp X) holds f is weakly*-convergent iff ( ||.f.|| is bounded & ex X0 be Subset of X st X0 is dense & (for x be Point of X st x in X0 holds (f # x) is convergent))

    proof

      let X be RealBanachSpace, f be sequence of ( DualSp X);

      now

        assume

         AS: f is weakly*-convergent;

        hence ||.f.|| is bounded by Th711;

        set X0 = ( [#] X);

        take X0;

        thus X0 is dense;

        thus for x be Point of X st x in X0 holds (f # x) is convergent by AS;

      end;

      hence thesis by Th712A;

    end;

    begin

    definition

      let X be RealNormSpace, X0 be non empty Subset of X;

      :: DUALSP03:def6

      attr X0 is weakly-sequentially-compact means for seq be sequence of X0 holds ex seq1 be sequence of X st seq1 is subsequence of seq & seq1 is weakly-convergent & ( w-lim seq1) in X;

    end

    

     Th713A: for X be RealBanachSpace, X0 be non empty Subset of X st X is non trivial & X is Reflexive & X0 is weakly-sequentially-compact holds ex S be non empty Subset of REAL st S = { ||.x.|| where x be Point of X : x in X0 } & S is bounded_above

    proof

      let X be RealBanachSpace, X0 be non empty Subset of X;

      assume

       AS1: X is non trivial & X is Reflexive;

      assume

       AS2: X0 is weakly-sequentially-compact;

      assume

       B1: not (ex S be non empty Subset of REAL st S = { ||.x.|| where x be Point of X : x in X0 } & S is bounded_above);

      set S = { ||.x.|| where x be Point of X : x in X0 };

      now

        let r be object;

        assume r in S;

        then ex x be Point of X st r = ||.x.|| & x in X0;

        hence r in REAL ;

      end;

      then

       A11: S c= REAL ;

      consider x0 be object such that

       A12: x0 in X0 by XBOOLE_0:def 1;

      reconsider x0 as Point of X by A12;

       ||.x0.|| in S by A12;

      then

      reconsider S as non empty Subset of REAL by A11;

      defpred P[ Nat, Point of X] means $1 <= ||.$2.|| & $2 in X0;

      

       P1: for n be Element of NAT holds ex x be Point of X st P[n, x]

      proof

        assume not (for n be Element of NAT holds ex x be Point of X st P[n, x]);

        then

        consider n be Element of NAT such that

         Q1: for x be Point of X holds not P[n, x];

        for r be ExtReal st r in S holds r <= n

        proof

          let r be ExtReal;

          assume r in S;

          then ex x be Point of X st r = ||.x.|| & x in X0;

          hence r <= n by Q1;

        end;

        then n is UpperBound of S by XXREAL_2:def 1;

        then S is bounded_above;

        hence contradiction by B1;

      end;

      consider seq0 be Function of NAT , the carrier of X such that

       P2: for n be Element of NAT holds P[n, (seq0 . n)] from FUNCT_2:sch 3( P1);

      

       P3: for n be Nat holds n <= ||.(seq0 . n).|| & (seq0 . n) in X0

      proof

        let n be Nat;

        n is Element of NAT by ORDINAL1:def 12;

        hence thesis by P2;

      end;

      for n be Element of NAT holds (seq0 . n) in X0 by P3;

      then ( rng seq0) c= X0 by FUNCT_2: 114;

      then

      reconsider seq = seq0 as sequence of X0 by FUNCT_2: 6;

      consider seq1 be sequence of X such that

       A3: seq1 is subsequence of seq & seq1 is weakly-convergent & ( w-lim seq1) in X by AS2;

       ||.seq1.|| is bounded by A3, AS1, Th79;

      then

      consider r be Real such that

       A4: for n be Nat holds ( ||.seq1.|| . n) < r by SEQ_2:def 3;

      set n = ( [/r\] + 1);

      ( ||.seq1.|| . 0 ) < r by A4;

      then ||.(seq1 . 0 ).|| < r by NORMSP_0:def 4;

      then 0 <= n by INT_1: 32;

      then n in NAT by INT_1: 3;

      then

      reconsider n as Nat;

      consider N be increasing sequence of NAT such that

       A52: seq1 = (seq * N) by A3, VALUED_0:def 17;

      set m = (N . n);

      (seq0 . m) = (seq1 . n) by A52, FUNCT_2: 15, ORDINAL1:def 12;

      then

       A54: (N . n) <= ||.(seq1 . n).|| by P3;

      n <= (N . n) by SEQM_3: 14;

      then

       B55: n <= ||.(seq1 . n).|| by A54, XXREAL_0: 2;

      ( ||.seq1.|| . n) < r by A4;

      then ||.(seq1 . n).|| < r by NORMSP_0:def 4;

      hence contradiction by B55, XXREAL_0: 2, INT_1: 32;

    end;

    theorem :: DUALSP03:19

    

     Lm813A: for X be RealNormSpace, x be sequence of X st X is Reflexive holds x is weakly-convergent iff (( BidualFunc X) * x) is weakly*-convergent

    proof

      let X be RealNormSpace, x be sequence of X;

      assume

       AS: X is Reflexive;

      set f = (( BidualFunc X) * x);

      hereby

        assume

         AS: x is weakly-convergent;

        reconsider x0 = ( w-lim x) as Point of X;

        for g be Point of ( DualSp X) holds (f # g) is convergent & ( lim (f # g)) = (( BiDual x0) . g)

        proof

          let g be Point of ( DualSp X);

          reconsider f0 = ( BiDual x0) as Point of ( DualSp ( DualSp X));

          

           A3: for n be Nat holds ((f # g) . n) = ((g * x) . n)

          proof

            let n be Nat;

            reconsider f1 = ( BiDual (x . n)) as Point of ( DualSp ( DualSp X));

            (f . n) = (( BidualFunc X) . (x . n)) by FUNCT_2: 15, ORDINAL1:def 12;

            then

             B2: (f . n) = ( BiDual (x . n)) by DUALSP02:def 2;

            ((f # g) . n) = ((f . n) . g) by Def1;

            then ((f # g) . n) = (g . (x . n)) by B2, DUALSP02:def 1;

            hence ((f # g) . n) = ((g * x) . n) by FUNCT_2: 15, ORDINAL1:def 12;

          end;

          reconsider g1 = g as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

           A41: (g1 * x) is convergent & ( lim (g1 * x)) = (g1 . x0) by DefWeaklim, AS;

          

           A5: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds |.(((f # g) . n) - (f0 . g)).| < r

          proof

            let r be Real;

            assume 0 < r;

            then

            consider m be Nat such that

             B1: for n be Nat st m <= n holds |.(((g1 * x) . n) - (g1 . x0)).| < r by A41, SEQ_2:def 7;

            take m;

            thus for n be Nat st m <= n holds |.(((f # g) . n) - (f0 . g)).| < r

            proof

              let n be Nat;

              assume

               C3: m <= n;

              (f0 . g) = (g . x0) by DUALSP02:def 1;

              then |.(((f # g) . n) - (f0 . g)).| = |.(((g1 * x) . n) - (g1 . x0)).| by A3;

              hence thesis by B1, C3;

            end;

          end;

          then (f # g) is convergent;

          hence thesis by A5, SEQ_2:def 7;

        end;

        hence f is weakly*-convergent;

      end;

      assume f is weakly*-convergent;

      then

      consider f0 be Point of ( DualSp ( DualSp X)) such that

       A0: for h be Point of ( DualSp X) holds (f # h) is convergent & ( lim (f # h)) = (f0 . h);

      consider x0 be Point of X such that

       A1: for g be Point of ( DualSp X) holds (f0 . g) = (g . x0) by AS, DUALSP02: 21;

      for g be Lipschitzian linear-Functional of X holds (g * x) is convergent & ( lim (g * x)) = (g . x0)

      proof

        let g be Lipschitzian linear-Functional of X;

        reconsider g1 = g as Point of ( DualSp X) by DUALSP01:def 10;

        

         A3: for n be Nat holds ((g * x) . n) = ((f # g1) . n)

        proof

          let n be Nat;

          reconsider f1 = ( BiDual (x . n)) as Point of ( DualSp ( DualSp X));

          

           B2: (f . n) = (( BidualFunc X) . (x . n)) by FUNCT_2: 15, ORDINAL1:def 12

          .= ( BiDual (x . n)) by DUALSP02:def 2;

          

          thus ((g * x) . n) = (g1 . (x . n)) by FUNCT_2: 15, ORDINAL1:def 12

          .= (f1 . g1) by DUALSP02:def 1

          .= ((f # g1) . n) by B2, Def1;

        end;

        

         B4: (f # g1) is convergent & ( lim (f # g1)) = (f0 . g1) by A0;

        

         A5: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds |.(((g * x) . n) - (g1 . x0)).| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

           B1: for n be Nat st m <= n holds |.(((f # g1) . n) - (f0 . g1)).| < r by SEQ_2:def 7, B4;

          take m;

          hereby

            let n be Nat;

            assume

             C3: m <= n;

            (f0 . g1) = (g1 . x0) by A1;

            then |.(((g * x) . n) - (g1 . x0)).| = |.(((f # g1) . n) - (f0 . g1)).| by A3;

            hence |.(((g * x) . n) - (g1 . x0)).| < r by B1, C3;

          end;

        end;

        then (g * x) is convergent;

        hence thesis by A5, SEQ_2:def 7;

      end;

      hence x is weakly-convergent;

    end;

    theorem :: DUALSP03:20

    

     Lm814A: for X be RealNormSpace, f be sequence of ( DualSp X), x be Point of X st ||.f.|| is bounded holds ex f0 be sequence of ( DualSp X) st f0 is subsequence of f & ||.f0.|| is bounded & (f0 # x) is convergent

    proof

      let X be RealNormSpace, f be sequence of ( DualSp X), x be Point of X;

      assume

       AS0: ||.f.|| is bounded;

      consider r0 be Real such that

       B0: 0 < r0 & for m be Nat holds |.( ||.f.|| . m).| < r0 by AS0, SEQ_2: 3;

      set r = ((r0 * ||.x.||) + 1);

      

       C1: (r0 * ||.x.||) < ((r0 * ||.x.||) + 1) by XREAL_1: 29;

      

       BY: for m be Nat holds |.((f # x) . m).| < r

      proof

        let m be Nat;

        reconsider h = (f . m) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

        

         B5: |.(h . x).| <= ( ||.(f . m).|| * ||.x.||) by DUALSP01: 26;

        

         B3: |.( ||.f.|| . m).| <= r0 by B0;

        ( ||.f.|| . m) = ||.(f . m).|| by NORMSP_0:def 4;

        then ||.(f . m).|| <= r0 by B3, ABSVALUE:def 1;

        then

         C6: ( ||.(f . m).|| * ||.x.||) <= (r0 * ||.x.||) by XREAL_1: 64;

         |.((f # x) . m).| = |.((f . m) . x).| by Def1;

        then |.((f # x) . m).| <= (r0 * ||.x.||) by B5, XXREAL_0: 2, C6;

        hence thesis by C1, XXREAL_0: 2;

      end;

      reconsider seq = (f # x) as Real_Sequence;

      consider seq1 be Real_Sequence such that

       X1: seq1 is subsequence of seq & seq1 is convergent by B0, SEQ_2: 3, BY, SEQ_4: 40;

      consider N be increasing sequence of NAT such that

       X2: seq1 = (seq * N) by X1, VALUED_0:def 17;

      set f0 = (f * N);

      for k be Nat holds ((f0 # x) . k) = (seq1 . k)

      proof

        let k be Nat;

        

        thus ((f0 # x) . k) = ((f0 . k) . x) by Def1

        .= ((f . (N . k)) . x) by ORDINAL1:def 12, FUNCT_2: 15

        .= ((f # x) . (N . k)) by Def1

        .= (seq1 . k) by X2, ORDINAL1:def 12, FUNCT_2: 15;

      end;

      then

       Y5: (f0 # x) = seq1;

      for n be Nat holds |.( ||.f0.|| . n).| < r0

      proof

        let n be Nat;

        

         Y2: (f0 . n) = (f . (N . n)) by ORDINAL1:def 12, FUNCT_2: 15;

        ( ||.f0.|| . n) = ||.(f0 . n).|| by NORMSP_0:def 4;

        then ( ||.f0.|| . n) = ( ||.f.|| . (N . n)) by Y2, NORMSP_0:def 4;

        hence thesis by B0;

      end;

      hence thesis by X1, Y5, B0, SEQ_2: 3;

    end;

    theorem :: DUALSP03:21

    

     Lm814A1: for X be RealNormSpace, f be sequence of ( DualSp X), x be Point of X st ||.f.|| is bounded holds ex f0 be sequence of ( DualSp X) st f0 is subsequence of f & ||.f0.|| is bounded & (f0 # x) is convergent & (f0 # x) is subsequence of (f # x)

    proof

      let X be RealNormSpace, f be sequence of ( DualSp X), x be Point of X;

      assume ||.f.|| is bounded;

      then

      consider r0 be Real such that

       B0: 0 < r0 & for m be Nat holds |.( ||.f.|| . m).| < r0 by SEQ_2: 3;

      set r = ((r0 * ||.x.||) + 1);

      

       BS: for m be Nat holds |.((f # x) . m).| < r

      proof

        let m be Nat;

        reconsider h = (f . m) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

         |.(h . x).| = |.((f # x) . m).| by Def1;

        then

         B5: |.((f # x) . m).| <= ( ||.(f . m).|| * ||.x.||) by DUALSP01: 26;

         |.( ||.f.|| . m).| <= r0 & ( ||.f.|| . m) = ||.(f . m).|| by B0, NORMSP_0:def 4;

        then ||.(f . m).|| <= r0 by ABSVALUE:def 1;

        then ( ||.(f . m).|| * ||.x.||) <= (r0 * ||.x.||) & (r0 * ||.x.||) < r by XREAL_1: 29, XREAL_1: 64;

        then ( ||.(f . m).|| * ||.x.||) < r by XXREAL_0: 2;

        hence thesis by B5, XXREAL_0: 2;

      end;

      reconsider seq = (f # x) as Real_Sequence;

      consider seq1 be Real_Sequence such that

       X1: seq1 is subsequence of seq & seq1 is convergent by B0, SEQ_2: 3, BS, SEQ_4: 40;

      consider N be increasing sequence of NAT such that

       X2: seq1 = (seq * N) by X1, VALUED_0:def 17;

      reconsider f0 = (f * N) as sequence of ( DualSp X);

      now

        let k be Nat;

        

        thus ((f0 # x) . k) = ((f0 . k) . x) by Def1

        .= ((f . (N . k)) . x) by ORDINAL1:def 12, FUNCT_2: 15

        .= ((f # x) . (N . k)) by Def1

        .= (seq1 . k) by X2, ORDINAL1:def 12, FUNCT_2: 15;

      end;

      then

       X5: (f0 # x) = seq1;

      for n be Nat holds |.( ||.f0.|| . n).| < r0

      proof

        let n be Nat;

        ( ||.f0.|| . n) = ||.(f0 . n).|| by NORMSP_0:def 4;

        then ( ||.f0.|| . n) = ||.(f . (N . n)).|| by ORDINAL1:def 12, FUNCT_2: 15;

        then ( ||.f0.|| . n) = ( ||.f.|| . (N . n)) by NORMSP_0:def 4;

        hence thesis by B0;

      end;

      hence thesis by X1, X5, B0, SEQ_2: 3;

    end;

    theorem :: DUALSP03:22

    

     Lm814A2: for X be RealNormSpace, f be sequence of ( DualSp X), x be Point of X st ||.f.|| is bounded holds ex f0 be sequence of ( DualSp X), N be increasing sequence of NAT st f0 is subsequence of f & ||.f0.|| is bounded & (f0 # x) is convergent & (f0 # x) is subsequence of (f # x) & f0 = (f * N)

    proof

      let X be RealNormSpace, f be sequence of ( DualSp X), x be Point of X;

      assume ||.f.|| is bounded;

      then

      consider f0 be sequence of ( DualSp X) such that

       A1: f0 is subsequence of f & ||.f0.|| is bounded & (f0 # x) is convergent & (f0 # x) is subsequence of (f # x) by Lm814A1;

      take f0;

      ex N be increasing sequence of NAT st f0 = (f * N) by A1, VALUED_0:def 17;

      hence thesis by A1;

    end;

    theorem :: DUALSP03:23

    for X be RealNormSpace, f be sequence of ( DualSp X), x be sequence of X st ||.f.|| is bounded holds ex F be sequence of ( Funcs ( NAT ,the carrier of ( DualSp X))) st (F . 0 ) is subsequence of f & ((F . 0 ) # (x . 0 )) is convergent & (for k be Nat holds (F . (k + 1)) is subsequence of (F . k)) & (for k be Nat holds ((F . (k + 1)) # (x . (k + 1))) is convergent)

    proof

      let X be RealNormSpace, f be sequence of ( DualSp X), x be sequence of X;

      assume

       AS: ||.f.|| is bounded;

      set D = ( Funcs ( NAT ,the carrier of ( DualSp X)));

      consider f0 be sequence of ( DualSp X) such that

       P0: f0 is subsequence of f & ||.f0.|| is bounded & (f0 # (x . 0 )) is convergent by AS, Lm814A;

      reconsider A = f0 as Element of D by FUNCT_2: 8;

      defpred P[ Nat, sequence of ( DualSp X), sequence of ( DualSp X)] means ||.$2.|| is bounded implies ($3 is subsequence of $2 & ||.$3.|| is bounded & ($3 # (x . ($1 + 1))) is convergent);

      

       P1: for n be Nat holds for z be Element of D holds ex y be Element of D st P[n, z, y]

      proof

        let n be Nat;

        let z be Element of D;

        consider f0 be sequence of ( DualSp X) such that

         X1: ||.z.|| is bounded implies f0 is subsequence of z & ||.f0.|| is bounded & (f0 # (x . (n + 1))) is convergent by Lm814A;

        reconsider y = f0 as Element of D by FUNCT_2: 8;

        take y;

        thus thesis by X1;

      end;

      consider F be sequence of D such that

       X2: (F . 0 ) = A & for n be Nat holds P[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( P1);

      defpred Q[ Nat] means (F . ($1 + 1)) is subsequence of (F . $1) & ||.(F . ($1 + 1)).|| is bounded & ((F . ($1 + 1)) # (x . ($1 + 1))) is convergent;

      

       Q0: Q[ 0 ] by X2, P0;

      

       Q1: for n be Nat st Q[n] holds Q[(n + 1)] by X2;

      

       Q2: for n be Nat holds Q[n] from NAT_1:sch 2( Q0, Q1);

      take F;

      thus thesis by P0, X2, Q2;

    end;

    theorem :: DUALSP03:24

    

     Lm814C: for X be RealNormSpace, f be sequence of ( DualSp X), x be sequence of X st ||.f.|| is bounded holds ex F be sequence of ( Funcs ( NAT ,the carrier of ( DualSp X))), N be sequence of ( Funcs ( NAT , NAT )) st (F . 0 ) is subsequence of f & ((F . 0 ) # (x . 0 )) is convergent & (N . 0 ) is increasing sequence of NAT & (F . 0 ) = (f * (N . 0 )) & (for k be Nat holds (F . (k + 1)) is subsequence of (F . k)) & (for k be Nat holds ((F . (k + 1)) # (x . (k + 1))) is convergent) & (for k be Nat holds ((F . (k + 1)) # (x . (k + 1))) is subsequence of ((F . k) # (x . (k + 1)))) & (for k be Nat holds (N . (k + 1)) is increasing sequence of NAT ) & for k be Nat holds (F . (k + 1)) = ((F . k) * (N . (k + 1)))

    proof

      let X be RealNormSpace, f be sequence of ( DualSp X), x be sequence of X;

      assume ||.f.|| is bounded;

      then

      consider f0 be sequence of ( DualSp X) such that

       P0: f0 is subsequence of f & ||.f0.|| is bounded & (f0 # (x . 0 )) is convergent & (f0 # (x . 0 )) is subsequence of (f # (x . 0 )) by Lm814A1;

      consider N0 be increasing sequence of NAT such that

       R0: f0 = (f * N0) by VALUED_0:def 17, P0;

      set D1 = ( Funcs ( NAT ,the carrier of ( DualSp X)));

      set D2 = ( Funcs ( NAT , NAT ));

      reconsider A = f0 as Element of D1 by FUNCT_2: 8;

      reconsider B = N0 as Element of D2 by FUNCT_2: 8;

      defpred P[ Nat, sequence of ( DualSp X), sequence of NAT , sequence of ( DualSp X), sequence of NAT ] means ||.$2.|| is bounded implies $4 is subsequence of $2 & ||.$4.|| is bounded & ($4 # (x . ($1 + 1))) is convergent & ($4 # (x . ($1 + 1))) is subsequence of ($2 # (x . ($1 + 1))) & $5 is increasing sequence of NAT & $4 = ($2 * $5);

      

       P1: for n be Nat holds for z be Element of D1, y be Element of D2 holds ex z1 be Element of D1, y1 be Element of D2 st P[n, z, y, z1, y1]

      proof

        let n be Nat;

        let z be Element of D1, y be Element of D2;

        consider f0 be sequence of ( DualSp X), N be increasing sequence of NAT such that

         X1: ||.z.|| is bounded implies f0 is subsequence of z & ||.f0.|| is bounded & (f0 # (x . (n + 1))) is convergent & (f0 # (x . (n + 1))) is subsequence of (z # (x . (n + 1))) & f0 = (z * N) by Lm814A2;

        reconsider z1 = f0 as Element of D1 by FUNCT_2: 8;

        reconsider y1 = N as Element of D2 by FUNCT_2: 8;

        take z1, y1;

        thus thesis by X1;

      end;

      consider F be sequence of D1, N be sequence of D2 such that

       X2: (F . 0 ) = A & (N . 0 ) = B & for n be Nat holds P[n, (F . n), (N . n), (F . (n + 1)), (N . (n + 1))] from RECDEF_2:sch 3( P1);

      defpred Q[ Nat] means ((F . ($1 + 1)) is subsequence of (F . $1) & ||.(F . ($1 + 1)).|| is bounded & ((F . ($1 + 1)) # (x . ($1 + 1))) is convergent & ((F . ($1 + 1)) # (x . ($1 + 1))) is subsequence of ((F . $1) # (x . ($1 + 1))) & (N . ($1 + 1)) is increasing sequence of NAT & (F . ($1 + 1)) = ((F . $1) * (N . ($1 + 1))));

      

       Q0: Q[ 0 ] by X2, P0;

      

       Q1: for n be Nat st Q[n] holds Q[(n + 1)] by X2;

      

       Q2: for n be Nat holds Q[n] from NAT_1:sch 2( Q0, Q1);

      take F, N;

      thus thesis by P0, X2, R0, Q2;

    end;

    theorem :: DUALSP03:25

    

     Lm814: for X be RealNormSpace, f be sequence of ( DualSp X), x be sequence of X st ||.f.|| is bounded holds ex M be sequence of ( DualSp X) st M is subsequence of f & for k be Nat holds (M # (x . k)) is convergent

    proof

      let X be RealNormSpace, f be sequence of ( DualSp X), x be sequence of X;

      assume ||.f.|| is bounded;

      then

      consider F be sequence of ( Funcs ( NAT ,the carrier of ( DualSp X))), N be sequence of ( Funcs ( NAT , NAT )) such that

       A0: (F . 0 ) is subsequence of f & ((F . 0 ) # (x . 0 )) is convergent & (N . 0 ) is increasing sequence of NAT & (F . 0 ) = (f * (N . 0 )) & (for k be Nat holds (F . (k + 1)) is subsequence of (F . k)) & (for k be Nat holds ((F . (k + 1)) # (x . (k + 1))) is convergent) & (for k be Nat holds ((F . (k + 1)) # (x . (k + 1))) is subsequence of ((F . k) # (x . (k + 1)))) & (for k be Nat holds (N . (k + 1)) is increasing sequence of NAT ) & for k be Nat holds (F . (k + 1)) = ((F . k) * (N . (k + 1))) by Lm814C;

      deffunc F1( Element of NAT ) = ((F . $1) . $1);

      consider M be Function of NAT , ( DualSp X) such that

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

      reconsider M as sequence of ( DualSp X);

      

       A2: for k be Nat holds (M . k) = ((F . k) . k)

      proof

        let k be Nat;

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

        (M . k1) = ((F . k1) . k1) by A1;

        hence thesis;

      end;

      set D = ( Funcs ( NAT , NAT ));

      reconsider A = (N . 0 ) as Element of D by FUNCT_2: 8;

      defpred P[ Nat, sequence of NAT , sequence of NAT ] means $3 = ($2 * (N . ($1 + 1)));

      

       P1: for n be Nat holds for x be Element of D holds ex y be Element of D st P[n, x, y]

      proof

        let n be Nat;

        let x be Element of D;

        reconsider y = (x * (N . (n + 1))) as Element of D by FUNCT_2: 8;

        take y;

        thus y = (x * (N . (n + 1)));

      end;

      consider J be sequence of D such that

       P2: (J . 0 ) = A & for n be Nat holds P[n, (J . n), (J . (n + 1))] from RECDEF_1:sch 2( P1);

      defpred Q[ Nat] means (J . $1) is increasing sequence of NAT ;

      

       Q0: Q[ 0 ] by P2, A0;

      

       Q1: for n be Nat st Q[n] holds Q[(n + 1)]

      proof

        let n be Nat;

        assume

         X10: Q[n];

        (N . (n + 1)) is increasing sequence of NAT by A0;

        then ((J . n) * (N . (n + 1))) is increasing sequence of NAT by X10;

        hence (J . (n + 1)) is increasing sequence of NAT by P2;

      end;

      

       Q2: for n be Nat holds Q[n] from NAT_1:sch 2( Q0, Q1);

      defpred P1[ Nat] means (F . $1) = (f * (J . $1));

      

       Q0: P1[ 0 ] by P2, A0;

      

       Q1: for n be Nat st P1[n] holds P1[(n + 1)]

      proof

        let n be Nat;

        assume

         X2: P1[n];

        (F . (n + 1)) = ((F . n) * (N . (n + 1))) by A0

        .= (f * ((J . n) * (N . (n + 1)))) by X2, RELAT_1: 36;

        hence (F . (n + 1)) = (f * (J . (n + 1))) by P2;

      end;

      

       A41: for n be Nat holds P1[n] from NAT_1:sch 2( Q0, Q1);

      deffunc F2( Element of NAT ) = ((J . $1) . $1);

      consider L be Function of NAT , NAT such that

       A5: for k be Element of NAT holds (L . k) = F2(k) from FUNCT_2:sch 4;

      reconsider L as sequence of NAT ;

      

       A6: for k be Nat holds (L . k) = ((J . k) . k)

      proof

        let k be Nat;

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

        (L . k1) = ((J . k1) . k1) by A5;

        hence thesis;

      end;

      reconsider L0 = L as Real_Sequence by FUNCT_2: 7, NUMBERS: 19;

      for k be Nat holds (L0 . k) < (L0 . (k + 1))

      proof

        let k be Nat;

        

         B2: (J . k) is increasing Real_Sequence by Q2, FUNCT_2: 7, NUMBERS: 19;

        

         B3: (L . (k + 1)) = ((J . (k + 1)) . (k + 1)) by A6

        .= (((J . k) * (N . (k + 1))) . (k + 1)) by P2

        .= ((J . k) . ((N . (k + 1)) . (k + 1))) by FUNCT_2: 15;

        (N . (k + 1)) is increasing sequence of NAT by A0;

        then (k + 1) <= ((N . (k + 1)) . (k + 1)) by SEQM_3: 14;

        then k < ((N . (k + 1)) . (k + 1)) by XREAL_1: 145;

        then ((J . k) . k) < ((J . k) . ((N . (k + 1)) . (k + 1))) by B2, SEQM_3: 1;

        hence thesis by B3, A6;

      end;

      then L0 is increasing;

      then

      reconsider L as increasing sequence of NAT ;

      for k be Nat holds (M . k) = ((f * L) . k)

      proof

        let k be Nat;

        (M . k) = ((F . k) . k) by A2

        .= ((f * (J . k)) . k) by A41

        .= (f . ((J . k) . k)) by ORDINAL1:def 12, FUNCT_2: 15

        .= (f . (L . k)) by A6;

        hence (M . k) = ((f * L) . k) by ORDINAL1:def 12, FUNCT_2: 15;

      end;

      then

       A71: M = (f * L);

      for k be Nat holds (M # (x . k)) is convergent

      proof

        let k be Nat;

        

         Q1: ((F . k) # (x . k)) is convergent

        proof

          per cases ;

            suppose k = 0 ;

            hence ((F . k) # (x . k)) is convergent by A0;

          end;

            suppose k <> 0 ;

            then ex n be Nat st k = (n + 1) by NAT_1: 6;

            hence ((F . k) # (x . k)) is convergent by A0;

          end;

        end;

        

         A0X: for k be Nat holds (N . k) is increasing sequence of NAT

        proof

          let k be Nat;

          per cases ;

            suppose k = 0 ;

            hence (N . k) is increasing sequence of NAT by A0;

          end;

            suppose k <> 0 ;

            then ex n be Nat st k = (n + 1) by NAT_1: 6;

            hence (N . k) is increasing sequence of NAT by A0;

          end;

        end;

        defpred PNk[ Nat, sequence of NAT ] means for i be Nat holds ($2 . i) = (((N . (k + $1)) . (k + i)) - k);

        

         P11: for n be Element of NAT holds ex y be Element of D st PNk[n, y]

        proof

          let n be Element of NAT ;

          defpred PNk1[ Nat, object] means $2 = (((N . (k + n)) . (k + $1)) - k);

          

           P111: for i be Element of NAT holds ex y be Element of NAT st PNk1[i, y]

          proof

            let i be Element of NAT ;

            

             B5: k <= (k + i) by NAT_1: 11;

            (N . (k + n)) is increasing sequence of NAT by A0X;

            then (k + i) <= ((N . (k + n)) . (k + i)) by SEQM_3: 14;

            then k <= ((N . (k + n)) . (k + i)) by B5, XXREAL_0: 2;

            then

            reconsider y = (((N . (k + n)) . (k + i)) - k) as Element of NAT by INT_1: 3, XREAL_1: 48;

            take y;

            thus y = (((N . (k + n)) . (k + i)) - k);

          end;

          consider y be Function of NAT , NAT such that

           P121: for i be Element of NAT holds PNk1[i, (y . i)] from FUNCT_2:sch 3( P111);

          reconsider y as Element of D by FUNCT_2: 8;

          take y;

          thus for i be Nat holds (y . i) = (((N . (k + n)) . (k + i)) - k)

          proof

            let i be Nat;

            i in NAT by ORDINAL1:def 12;

            hence (y . i) = (((N . (k + n)) . (k + i)) - k) by P121;

          end;

        end;

        consider Nk be Function of NAT , D such that

         P12: for n be Element of NAT holds PNk[n, (Nk . n)] from FUNCT_2:sch 3( P11);

        

         P13: for n be Element of NAT holds (Nk . n) is increasing sequence of NAT

        proof

          let n be Element of NAT ;

          reconsider Nkn = (Nk . n) as Real_Sequence by FUNCT_2: 7, NUMBERS: 19;

          

           D1: (N . (k + n)) is increasing Real_Sequence by FUNCT_2: 7, NUMBERS: 19, A0X;

          for i be Nat holds (Nkn . i) < (Nkn . (i + 1))

          proof

            let i be Nat;

            

             D2: ((Nk . n) . i) = (((N . (k + n)) . (k + i)) - k) & ((Nk . n) . (i + 1)) = (((N . (k + n)) . (k + (i + 1))) - k) by P12;

            (((N . (k + n)) . (k + i)) - k) < (((N . (k + n)) . ((k + i) + 1)) - k) by XREAL_1: 14, D1, SEQM_3:def 6;

            hence thesis by D2;

          end;

          hence (Nk . n) is increasing sequence of NAT by SEQM_3:def 6;

        end;

        

         A0k: for n be Nat holds ((F . (k + (n + 1))) ^\ k) = (((F . (k + n)) ^\ k) * (Nk . (n + 1)))

        proof

          let n be Nat;

          

           XX1: (F . ((k + 1) + n)) = ((F . (k + n)) * (N . ((k + n) + 1))) by A0;

          for i be Nat holds ((((F . (k + n)) ^\ k) * (Nk . (n + 1))) . i) = ((((F . (k + n)) * (N . ((k + n) + 1))) ^\ k) . i)

          proof

            let i be Nat;

            

             N3: ((Nk . (n + 1)) . i) = (((N . (k + (n + 1))) . (k + i)) - k) by P12;

            

            thus ((((F . (k + n)) ^\ k) * (Nk . (n + 1))) . i) = (((F . (k + n)) ^\ k) . ((Nk . (n + 1)) . i)) by FUNCT_2: 15, ORDINAL1:def 12

            .= ((F . (k + n)) . (k + (((N . (k + (n + 1))) . (k + i)) - k))) by NAT_1:def 3, N3

            .= (((F . (k + n)) * (N . (k + (n + 1)))) . (k + i)) by FUNCT_2: 15, ORDINAL1:def 12

            .= ((((F . (k + n)) * (N . ((k + n) + 1))) ^\ k) . i) by NAT_1:def 3;

          end;

          hence thesis by XX1;

        end;

        reconsider Ak = ( id NAT ) as Element of D by FUNCT_2: 8;

        defpred PJk[ Nat, sequence of NAT , sequence of NAT ] means $3 = ($2 * (Nk . ($1 + 1)));

        

         P14: for n be Nat holds for x be Element of D holds ex y be Element of D st PJk[n, x, y]

        proof

          let n be Nat;

          let x be Element of D;

          reconsider y = (x * (Nk . (n + 1))) as Element of D by FUNCT_2: 8;

          take y;

          thus y = (x * (Nk . (n + 1)));

        end;

        consider Jk be sequence of D such that

         P15: (Jk . 0 ) = Ak & for n be Nat holds PJk[n, (Jk . n), (Jk . (n + 1))] from RECDEF_1:sch 2( P14);

        defpred QJk[ Nat] means (Jk . $1) is increasing sequence of NAT ;

        

         QJ0: QJk[ 0 ] by P15;

        

         QJ1: for n be Nat st QJk[n] holds QJk[(n + 1)]

        proof

          let n be Nat;

          assume

           X10: QJk[n];

          (Nk . (n + 1)) is increasing sequence of NAT by P13;

          then ((Jk . n) * (Nk . (n + 1))) is increasing sequence of NAT by X10;

          hence (Jk . (n + 1)) is increasing sequence of NAT by P15;

        end;

        

         AJ32: for n be Nat holds QJk[n] from NAT_1:sch 2( QJ0, QJ1);

        defpred P1Jk[ Nat] means ((F . (k + $1)) ^\ k) = (((F . k) ^\ k) * (Jk . $1));

        

         QJ0: P1Jk[ 0 ] by P15, FUNCT_2: 17;

        

         QJ1: for n be Nat st P1Jk[n] holds P1Jk[(n + 1)]

        proof

          let n be Nat;

          assume

           X2: P1Jk[n];

          

          thus ((F . (k + (n + 1))) ^\ k) = (((F . (k + n)) ^\ k) * (Nk . (n + 1))) by A0k

          .= (((F . k) ^\ k) * ((Jk . n) * (Nk . (n + 1)))) by X2, RELAT_1: 36

          .= (((F . k) ^\ k) * (Jk . (n + 1))) by P15;

        end;

        

         BJ4: for n be Nat holds P1Jk[n] from NAT_1:sch 2( QJ0, QJ1);

        deffunc FJk2( Element of NAT ) = ((Jk . $1) . $1);

        consider Lk be Function of NAT , NAT such that

         AJ5: for n be Element of NAT holds (Lk . n) = FJk2(n) from FUNCT_2:sch 4;

        reconsider Lk as sequence of NAT ;

        

         AJ6: for k be Nat holds (Lk . k) = ((Jk . k) . k)

        proof

          let k be Nat;

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

          (Lk . k1) = ((Jk . k1) . k1) by AJ5;

          hence thesis;

        end;

        reconsider L0k = Lk as Real_Sequence by FUNCT_2: 7, NUMBERS: 19;

        for k be Nat holds (L0k . k) < (L0k . (k + 1))

        proof

          let k be Nat;

          

           B2: (Jk . k) is increasing Real_Sequence by AJ32, FUNCT_2: 7, NUMBERS: 19;

          

           B3: (Lk . (k + 1)) = ((Jk . (k + 1)) . (k + 1)) by AJ6

          .= (((Jk . k) * (Nk . (k + 1))) . (k + 1)) by P15

          .= ((Jk . k) . ((Nk . (k + 1)) . (k + 1))) by FUNCT_2: 15;

          (Nk . (k + 1)) is increasing sequence of NAT by P13;

          then (k + 1) <= ((Nk . (k + 1)) . (k + 1)) by SEQM_3: 14;

          then k < ((Nk . (k + 1)) . (k + 1)) by XREAL_1: 145;

          then ((Jk . k) . k) < ((Jk . k) . ((Nk . (k + 1)) . (k + 1))) by B2, SEQM_3: 1;

          hence thesis by B3, AJ6;

        end;

        then L0k is increasing;

        then

        reconsider Lk as increasing sequence of NAT ;

        for n be Nat holds ((M ^\ k) . n) = ((((F . k) ^\ k) * Lk) . n)

        proof

          let n be Nat;

          

          thus ((M ^\ k) . n) = (M . (k + n)) by NAT_1:def 3

          .= ((F . (k + n)) . (k + n)) by A2

          .= (((F . (k + n)) ^\ k) . n) by NAT_1:def 3

          .= ((((F . k) ^\ k) * (Jk . n)) . n) by BJ4

          .= (((F . k) ^\ k) . ((Jk . n) . n)) by ORDINAL1:def 12, FUNCT_2: 15

          .= (((F . k) ^\ k) . (Lk . n)) by AJ6

          .= ((((F . k) ^\ k) * Lk) . n) by ORDINAL1:def 12, FUNCT_2: 15;

        end;

        then

         P11: (M ^\ k) = (((F . k) ^\ k) * Lk);

        

         Q12: for n be Nat holds (((M ^\ k) # (x . k)) . n) = (((M # (x . k)) ^\ k) . n)

        proof

          let n be Nat;

          

          thus (((M ^\ k) # (x . k)) . n) = (((M ^\ k) . n) . (x . k)) by Def1

          .= ((M . (k + n)) . (x . k)) by NAT_1:def 3

          .= ((M # (x . k)) . (k + n)) by Def1

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

        end;

        for n be Nat holds (((((F . k) ^\ k) * Lk) # (x . k)) . n) = (((((F . k) ^\ k) # (x . k)) * Lk) . n)

        proof

          let n be Nat;

          

          thus (((((F . k) ^\ k) * Lk) # (x . k)) . n) = (((((F . k) ^\ k) * Lk) . n) . (x . k)) by Def1

          .= ((((F . k) ^\ k) . (Lk . n)) . (x . k)) by ORDINAL1:def 12, FUNCT_2: 15

          .= ((((F . k) ^\ k) # (x . k)) . (Lk . n)) by Def1

          .= (((((F . k) ^\ k) # (x . k)) * Lk) . n) by ORDINAL1:def 12, FUNCT_2: 15;

        end;

        then ((((F . k) ^\ k) * Lk) # (x . k)) = ((((F . k) ^\ k) # (x . k)) * Lk);

        then

         Q2: ((M # (x . k)) ^\ k) = ((((F . k) ^\ k) # (x . k)) * Lk) by P11, Q12;

        for n be Nat holds ((((F . k) # (x . k)) ^\ k) . n) = ((((F . k) ^\ k) # (x . k)) . n)

        proof

          let n be Nat;

          

          thus ((((F . k) # (x . k)) ^\ k) . n) = (((F . k) # (x . k)) . (k + n)) by NAT_1:def 3

          .= (((F . k) . (k + n)) . (x . k)) by Def1

          .= ((((F . k) ^\ k) . n) . (x . k)) by NAT_1:def 3

          .= ((((F . k) ^\ k) # (x . k)) . n) by Def1;

        end;

        then (((F . k) # (x . k)) ^\ k) = (((F . k) ^\ k) # (x . k));

        then ((M # (x . k)) ^\ k) is convergent by Q1, Q2, SEQ_4: 16;

        hence (M # (x . k)) is convergent by SEQ_4: 21;

      end;

      hence thesis by A71;

    end;

    theorem :: DUALSP03:26

    

     Th814: for X be RealBanachSpace, f be sequence of ( DualSp X) st X is separable & ||.f.|| is bounded holds ex f0 be sequence of ( DualSp X) st f0 is subsequence of f & f0 is weakly*-convergent

    proof

      let X be RealBanachSpace, f be sequence of ( DualSp X);

      assume that

       A1: X is separable and

       A2: ||.f.|| is bounded;

      consider x0 be sequence of X such that

       A3: ( rng x0) is dense by A1, NORMSP_3: 21;

      set X0 = ( rng x0);

      consider f0 be sequence of ( DualSp X) such that

       AX: f0 is subsequence of f and

       A31: for n be Nat holds (f0 # (x0 . n)) is convergent by A2, Lm814;

      

       A21: for x be Point of X holds ex K be Real st 0 <= K & for n be Nat holds |.((f # x) . n).| <= K

      proof

        let x be Point of X;

        consider K0 be Real such that

         B0: 0 < K0 & for n be Nat holds |.( ||.f.|| . n).| < K0 by A2, SEQ_2: 3;

        reconsider K = ((K0 * ||.x.||) + 1) as Real;

        take K;

        

         B11: ((K0 * ||.x.||) + 0 ) < ((K0 * ||.x.||) + 1) by XREAL_1: 8;

        thus 0 <= K by B0;

        thus for n be Nat holds |.((f # x) . n).| <= K

        proof

          let n be Nat;

          

           B2: |.( ||.f.|| . n).| <= K0 by B0;

          ( ||.f.|| . n) = ||.(f . n).|| by NORMSP_0:def 4;

          then

           B3: ||.(f . n).|| <= K0 by B2, ABSVALUE:def 1;

          reconsider h = (f . n) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

           B4: |.(h . x).| <= ( ||.(f . n).|| * ||.x.||) by DUALSP01: 26;

          

           B51: ( ||.(f . n).|| * ||.x.||) <= (K0 * ||.x.||) by B3, XREAL_1: 64;

           |.((f # x) . n).| = |.((f . n) . x).| by Def1;

          then |.((f # x) . n).| <= (K0 * ||.x.||) by B51, B4, XXREAL_0: 2;

          hence thesis by B11, XXREAL_0: 2;

        end;

      end;

      set T = ( rng f0);

      consider N be increasing sequence of NAT such that

       AY: f0 = (f * N) by AX, VALUED_0:def 17;

      for x be Point of X holds ex K be Real st 0 <= K & for g be Point of ( DualSp X) st g in T holds |.(g . x).| <= K

      proof

        let x be Point of X;

        consider K be Real such that

         A4: 0 <= K & for n be Nat holds |.((f # x) . n).| <= K by A21;

        

         A5: for n be Nat holds |.((f0 # x) . n).| <= K

        proof

          let n be Nat;

          

           B3: (f0 . n) = (f . (N . n)) by AY, ORDINAL1:def 12, FUNCT_2: 15;

          reconsider n0 = (N . n) as Nat;

          ((f0 # x) . n) = ((f0 . n) . x) by Def1

          .= ((f # x) . n0) by B3, Def1;

          hence thesis by A4;

        end;

        for g be Point of ( DualSp X) st g in T holds |.(g . x).| <= K

        proof

          let g be Point of ( DualSp X);

          assume g in T;

          then

          consider n be object such that

           B1: n in NAT & g = (f0 . n) by FUNCT_2: 11;

          reconsider n as Nat by B1;

          (g . x) = ((f0 # x) . n) by B1, Def1;

          hence thesis by A5;

        end;

        hence thesis by A4;

      end;

      then

      consider L be Real such that

       A7: 0 <= L & for g be Point of ( DualSp X) st g in T holds ||.g.|| <= L by Lm55;

      set M = (L + 1);

      

       A8: (L + 0 ) < M by XREAL_1: 8;

      

       A9: for g be Lipschitzian linear-Functional of X st g in T holds for x,y be Point of X holds |.((g . x) - (g . y)).| <= (M * ||.(x - y).||)

      proof

        let g be Lipschitzian linear-Functional of X;

        reconsider g1 = g as Point of ( DualSp X) by DUALSP01:def 10;

        assume g in T;

        then ||.g1.|| <= L by A7;

        then

         B1: ||.g1.|| < M by A8, XXREAL_0: 2;

        let x,y be Point of X;

         |.((g . x) - (g . y)).| = |.((g . x) + (( - 1) * (g . y))).|;

        then |.((g . x) - (g . y)).| = |.((g . x) + (g . (( - 1) * y))).| by HAHNBAN:def 3;

        then |.((g . x) - (g . y)).| = |.(g . (x + (( - 1) * y))).| by HAHNBAN:def 2;

        then

         B2: |.((g . x) - (g . y)).| = |.(g . (x - y)).| by RLVECT_1: 16;

        

         B3: |.(g . (x - y)).| <= ( ||.g1.|| * ||.(x - y).||) by DUALSP01: 26;

        ( ||.g1.|| * ||.(x - y).||) <= (M * ||.(x - y).||) by B1, XREAL_1: 64;

        hence thesis by B2, B3, XXREAL_0: 2;

      end;

      

       BX: for x be Point of X holds (f0 # x) is convergent

      proof

        let x be Point of X;

        for TK1 be Real st TK1 > 0 holds ex m be Nat st for n be Nat st n >= m holds |.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1

        proof

          let TK1 be Real;

          assume

           B1: TK1 > 0 ;

          then

           C2: 0 < (TK1 / (3 * M)) by A7;

          set V = { z where z be Point of X : ||.(x - z).|| < (TK1 / (3 * M)) };

          V c= the carrier of X

          proof

            let s be object;

            assume s in V;

            then ex z be Point of X st s = z & ||.(x - z).|| < (TK1 / (3 * M));

            hence thesis;

          end;

          then

          reconsider V as Subset of X;

          reconsider TKK = TK1 as Real;

          V is open Subset of ( TopSpaceNorm X) by NORMSP_2: 8;

          then

           B31: V is open by NORMSP_2: 16;

           ||.(x - x).|| < (TKK / (3 * M)) by C2, NORMSP_1: 6;

          then x in V;

          then

          consider s be object such that

           B3: s in X0 & s in V by XBOOLE_0: 3, B31, A3, NORMSP_3: 17;

          consider y be Point of X such that

           B4: s = y & ||.(x - y).|| < (TK1 / (3 * M)) by B3;

          consider m be Element of NAT such that

           B40: s = (x0 . m) by B3, FUNCT_2: 113;

          consider m be Nat such that

           B5: for n be Nat st m <= n holds |.(((f0 # y) . n) - ((f0 # y) . m)).| < (TK1 / 3) by B1, A31, SEQ_4: 41, B4, B40;

          take m;

          for n be Nat st n >= m holds |.(((f0 # x) . n) - ((f0 # x) . m)).| < TK1

          proof

            let n be Nat;

            

             B6: m in NAT by ORDINAL1:def 12;

            

             B7: n in NAT by ORDINAL1:def 12;

            reconsider g = (f0 . n) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

            reconsider h = (f0 . m) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

            

             B8: ( |.(((f0 # x) . n) - ((f0 # y) . m)).| + |.(((f0 # y) . m) - ((f0 # x) . m)).|) <= (( |.(((f0 # x) . n) - ((f0 # y) . n)).| + |.(((f0 # y) . n) - ((f0 # y) . m)).|) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) by XREAL_1: 6, COMPLEX1: 63;

            assume n >= m;

            then |.(((f0 # y) . n) - ((f0 # y) . m)).| < (TK1 / 3) by B5;

            then ( |.(((f0 # x) . n) - ((f0 # y) . n)).| + |.(((f0 # y) . n) - ((f0 # y) . m)).|) < ( |.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) by XREAL_1: 8;

            then

             B9: (( |.(((f0 # x) . n) - ((f0 # y) . n)).| + |.(((f0 # y) . n) - ((f0 # y) . m)).|) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) < (( |.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) by XREAL_1: 8;

             |.(((f0 # x) . m) - ((f0 # y) . m)).| = |.(((f0 . m) . x) - ((f0 # y) . m)).| by Def1;

            then |.(((f0 # x) . m) - ((f0 # y) . m)).| = |.((h . x) - (h . y)).| by Def1;

            then

             B10: |.(((f0 # x) . m) - ((f0 # y) . m)).| <= (M * ||.(x - y).||) by A9, FUNCT_2: 4, B6;

            (M * ||.(x - y).||) < (M * (TK1 / (3 * M))) by A7, B4, XREAL_1: 68;

            then (M * ||.(x - y).||) < (TK1 / 3) by A7, XCMPLX_1: 92;

            then |.(((f0 # x) . m) - ((f0 # y) . m)).| < (TK1 / 3) by B10, XXREAL_0: 2;

            then |.(((f0 # y) . m) - ((f0 # x) . m)).| < (TK1 / 3) by COMPLEX1: 60;

            then

             B11: (((TK1 / 3) + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) < (((TK1 / 3) + (TK1 / 3)) + (TK1 / 3)) by XREAL_1: 8;

             |.(((f0 # x) . n) - ((f0 # y) . n)).| = |.(((f0 . n) . x) - ((f0 # y) . n)).| by Def1;

            then |.(((f0 # x) . n) - ((f0 # y) . n)).| = |.((g . x) - (g . y)).| by Def1;

            then

             B12: |.(((f0 # x) . n) - ((f0 # y) . n)).| <= (M * ||.(x - y).||) by A9, FUNCT_2: 4, B7;

             |.(((f0 # x) . n) - ((f0 # x) . m)).| <= ( |.(((f0 # x) . n) - ((f0 # y) . m)).| + |.(((f0 # y) . m) - ((f0 # x) . m)).|) by COMPLEX1: 63;

            then |.(((f0 # x) . n) - ((f0 # x) . m)).| <= (( |.(((f0 # x) . n) - ((f0 # y) . n)).| + |.(((f0 # y) . n) - ((f0 # y) . m)).|) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) by B8, XXREAL_0: 2;

            then

             B13: |.(((f0 # x) . n) - ((f0 # x) . m)).| < (( |.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) by B9, XXREAL_0: 2;

            (M * ||.(x - y).||) < (M * (TK1 / (3 * M))) by A7, B4, XREAL_1: 68;

            then (M * ||.(x - y).||) < (TK1 / 3) by A7, XCMPLX_1: 92;

            then |.(((f0 # x) . n) - ((f0 # y) . n)).| < (TK1 / 3) by B12, XXREAL_0: 2;

            then ( |.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) < ((TK1 / 3) + (TK1 / 3)) by XREAL_1: 8;

            then (( |.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) < (((TK1 / 3) + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) by XREAL_1: 8;

            then (( |.(((f0 # x) . n) - ((f0 # y) . n)).| + (TK1 / 3)) + |.(((f0 # y) . m) - ((f0 # x) . m)).|) < (((TK1 / 3) + (TK1 / 3)) + (TK1 / 3)) by B11, XXREAL_0: 2;

            hence thesis by B13, XXREAL_0: 2;

          end;

          hence thesis;

        end;

        hence thesis by SEQ_4: 41;

      end;

      defpred FP[ Element of the carrier of X, object] means $2 = ( lim (f0 # $1));

      

       C01: for x be Element of the carrier of X holds ex y be Element of REAL st FP[x, y]

      proof

        let x be Element of the carrier of X;

        ( lim (f0 # x)) in REAL by XREAL_0:def 1;

        hence thesis;

      end;

      consider f1 be Function of the carrier of X, REAL such that

       C0: for x be Element of the carrier of X holds FP[x, (f1 . x)] from FUNCT_2:sch 3( C01);

      

       C2: f1 is additive

      proof

        let x,y be Point of X;

         D11:

        now

          let n be Nat;

          reconsider h = (f0 . n) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

          thus ((f0 # (x + y)) . n) = ((f0 . n) . (x + y)) by Def1

          .= ((h . x) + (h . y)) by HAHNBAN:def 2

          .= (((f0 # x) . n) + ((f0 . n) . y)) by Def1

          .= (((f0 # x) . n) + ((f0 # y) . n)) by Def1;

        end;

        

         D2: (f0 # x) is convergent & (f0 # y) is convergent by BX;

        

        thus (f1 . (x + y)) = ( lim (f0 # (x + y))) by C0

        .= ( lim ((f0 # x) + (f0 # y))) by D11, SEQ_1: 7

        .= (( lim (f0 # x)) + ( lim (f0 # y))) by D2, SEQ_2: 6

        .= ((f1 . x) + ( lim (f0 # y))) by C0

        .= ((f1 . x) + (f1 . y)) by C0;

      end;

      

       C31: f1 is homogeneous

      proof

        let x be Point of X, r be Real;

         D31:

        now

          let n be Nat;

          reconsider h = (f0 . n) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

          thus ((f0 # (r * x)) . n) = ((f0 . n) . (r * x)) by Def1

          .= (r * (h . x)) by HAHNBAN:def 3

          .= (r * ((f0 # x) . n)) by Def1;

        end;

        

        thus (f1 . (r * x)) = ( lim (f0 # (r * x))) by C0

        .= ( lim (r (#) (f0 # x))) by D31, SEQ_1: 9

        .= (r * ( lim (f0 # x))) by BX, SEQ_2: 8

        .= (r * (f1 . x)) by C0;

      end;

      consider M be Real such that

       C4: 0 < M & for n be Nat holds |.( ||.f.|| . n).| < M by A2, SEQ_2: 3;

      now

        let x be Point of X;

        

         D5: (f0 # x) is convergent by BX;

        

         D7: |.(f1 . x).| = |.( lim (f0 # x)).| by C0

        .= ( lim |.(f0 # x).|) by BX, SEQ_4: 14;

        

         D8: for n be Nat holds ||.(f0 . n).|| <= M

        proof

          let n be Nat;

          (f0 . n) = (f . (N . n)) by AY, ORDINAL1:def 12, FUNCT_2: 15;

          then

           E3: ||.(f0 . n).|| = ( ||.f.|| . (N . n)) by NORMSP_0:def 4;

           |.( ||.f.|| . (N . n)).| < M by C4;

          hence thesis by E3, ABSVALUE:def 1;

        end;

        reconsider s = (M * ||.x.||) as Real;

         D91:

        now

          let n be Nat;

          reconsider h = (f0 . n) as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

           E3: |.(h . x).| <= ( ||.(f0 . n).|| * ||.x.||) by DUALSP01: 26;

          ( ||.(f0 . n).|| * ||.x.||) <= (M * ||.x.||) by XREAL_1: 64, D8;

          then |.(h . x).| <= (M * ||.x.||) by E3, XXREAL_0: 2;

          then

           E51: |.((f0 # x) . n).| <= (M * ||.x.||) by Def1;

          (( seq_const s) . n) = s by SEQ_1: 57;

          hence ( |.(f0 # x).| . n) <= (( seq_const s) . n) by E51, SEQ_1: 12;

        end;

        ( lim ( seq_const s)) = (( seq_const s) . 0 ) by SEQ_4: 26

        .= s;

        hence |.(f1 . x).| <= (M * ||.x.||) by D7, D91, D5, SEQ_2: 18;

      end;

      then f1 is Lipschitzian by C4;

      then f1 is Point of ( DualSp X) by DUALSP01:def 10, C31, C2;

      then f0 is weakly*-convergent by BX, C0;

      hence thesis by AX;

    end;

    theorem :: DUALSP03:27

    

     Th813: for X be RealBanachSpace, x be sequence of X st X is Reflexive & ||.x.|| is bounded holds ex x0 be sequence of X st x0 is subsequence of x & x0 is weakly-convergent

    proof

      let X be RealBanachSpace, x be sequence of X;

      assume that

       A2: X is Reflexive and

       A3: ||.x.|| is bounded;

      set L = ( ClNLin ( rng x));

      reconsider L0 = the carrier of L as Subset of X by DUALSP01:def 16;

      

       LM1: for z be object st z in ( rng x) holds z in the carrier of L

      proof

        let z be object;

        assume z in ( rng x);

        then

         C14: z in ( Lin ( rng x)) by RLVECT_3: 15;

        ex Z be Subset of X st Z = the carrier of ( Lin ( rng x)) & L = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),X)), ( Add_ (( Cl Z),X)), ( Mult_ (( Cl Z),X)), ( Norm_ (( Cl Z),X)) #) by NORMSP_3:def 20;

        hence z in the carrier of L by NORMSP_3: 4, C14, TARSKI:def 3;

      end;

      per cases ;

        suppose

         XX1: ( rng x) c= {( 0. X)};

        take x;

        thus x is subsequence of x by VALUED_0: 19;

        thus x is weakly-convergent by XX1, WEAKLM1;

      end;

        suppose not ( rng x) c= {( 0. X)};

        then

        consider z be object such that

         B11: z in ( rng x) & not z in {( 0. X)};

        

         B12: z in ( rng x) & z <> ( 0. X) by B11, TARSKI:def 1;

        

         B17: z in the carrier of L by LM1, B11;

        ( 0. X) = ( 0. L) by DUALSP01:def 16;

        then

         A11: L is non trivial by B12, B17;

        

         A12: L is Reflexive by A2, NORMSP_4: 29;

        ( DualSp ( DualSp L)) is separable by A11, A12, NORMSP_4: 25;

        then

         A4: ( DualSp L) is separable by Th73;

        set F = ( BidualFunc L);

        ( rng x) c= the carrier of L by LM1;

        then

        reconsider x1 = x as sequence of L by FUNCT_2: 6;

        for i be Nat holds ( ||.x1.|| . i) = ( ||.x.|| . i)

        proof

          let i be Nat;

          

          thus ( ||.x1.|| . i) = ||.(x1 . i).|| by NORMSP_0:def 4

          .= ||.(x . i).|| by NORMSP_3: 28

          .= ( ||.x.|| . i) by NORMSP_0:def 4;

        end;

        then

         B13: ||.x1.|| = ||.x.||;

        then

        consider r be Real such that

         A5: for n be Nat holds ( ||.x1.|| . n) < r by A3, SEQ_2:def 3;

        for n be Nat holds ( ||.(F * x1).|| . n) < r

        proof

          let n be Nat;

          

           C2: ( ||.x1.|| . n) < r by A5;

           ||.(x1 . n).|| = ||.(F . (x1 . n)).|| by A11, DUALSP02: 9;

          then ||.(F . (x1 . n)).|| < r by C2, NORMSP_0:def 4;

          then ||.((F * x1) . n).|| < r by ORDINAL1:def 12, FUNCT_2: 15;

          hence thesis by NORMSP_0:def 4;

        end;

        then

         A6: ||.(F * x1).|| is bounded_above;

        consider s be Real such that

         A7: for n be Nat holds s < ( ||.x1.|| . n) by B13, A3, SEQ_2:def 4;

        for n be Nat holds s < ( ||.(F * x1).|| . n)

        proof

          let n be Nat;

          

           C4: s < ( ||.x1.|| . n) by A7;

           ||.(x1 . n).|| = ||.(F . (x1 . n)).|| by A11, DUALSP02: 9;

          then s < ||.(F . (x1 . n)).|| by C4, NORMSP_0:def 4;

          then s < ||.((F * x1) . n).|| by ORDINAL1:def 12, FUNCT_2: 15;

          hence thesis by NORMSP_0:def 4;

        end;

        then ||.(F * x1).|| is bounded_below;

        then

        consider f1 be sequence of ( DualSp ( DualSp L)) such that

         A9: f1 is subsequence of (F * x1) & f1 is weakly*-convergent by A4, A6, Th814;

        consider L1 be increasing sequence of NAT such that

         A91: f1 = ((F * x1) * L1) by A9, VALUED_0:def 17;

        reconsider x01 = (x1 * L1) as sequence of L;

        f1 = (F * x01) by A91, RELAT_1: 36;

        then

         HX: x01 is weakly-convergent by A9, A12, Lm813A;

        

         BX: the carrier of L c= the carrier of X by DUALSP01:def 16;

        then

        reconsider x0 = x01 as sequence of X by FUNCT_2: 7;

        reconsider y = ( w-lim x01) as Point of X by BX;

        for h be Lipschitzian linear-Functional of X holds (h * x0) is convergent & ( lim (h * x0)) = (h . y)

        proof

          let h be Lipschitzian linear-Functional of X;

          reconsider h1 = (h | the carrier of L) as Lipschitzian linear-Functional of L by NORMSP_4: 22;

          

           GX3: ( dom h1) = the carrier of L by FUNCT_2:def 1;

          then ( rng x01) c= ( dom h1);

          then

           GX2: (h1 * x01) = (h * x0) by RELAT_1: 165;

          (h1 * x01) is convergent & ( lim (h1 * x01)) = (h1 . ( w-lim x01)) by HX, DefWeaklim;

          hence thesis by GX2, GX3, FUNCT_1: 47;

        end;

        then x0 is weakly-convergent;

        hence thesis;

      end;

    end;

    theorem :: DUALSP03:28

    for X be RealBanachSpace, X0 be non empty Subset of X st X is non trivial Reflexive holds X0 is weakly-sequentially-compact iff ex S be non empty Subset of REAL st S = { ||.x.|| where x be Point of X : x in X0 } & S is bounded_above

    proof

      let X be RealBanachSpace, X0 be non empty Subset of X;

      assume

       AS: X is non trivial Reflexive;

      hence X0 is weakly-sequentially-compact implies ex S be non empty Subset of REAL st S = { ||.x.|| where x be Point of X : x in X0 } & S is bounded_above by Th713A;

      given S be non empty Subset of REAL such that

       B0: S = { ||.x.|| where x be Point of X : x in X0 } & S is bounded_above;

      for seq be sequence of X0 holds ex seq1 be sequence of X st seq1 is subsequence of seq & seq1 is weakly-convergent & ( w-lim seq1) in X

      proof

        let seq0 be sequence of X0;

        reconsider seq = seq0 as sequence of X by FUNCT_2: 7;

        consider r be Real such that

         B1: r is UpperBound of S by B0;

        

         B2: (r + 0 ) < (r + 1) by XREAL_1: 8;

        for n be Nat holds ( ||.seq.|| . n) < (r + 1)

        proof

          let n be Nat;

          (seq0 . n) in X0;

          then ||.(seq . n).|| in S by B0;

          then ||.(seq . n).|| <= r by B1, XXREAL_2:def 1;

          then ( ||.seq.|| . n) <= r by NORMSP_0:def 4;

          hence thesis by B2, XXREAL_0: 2;

        end;

        then

         B5: ||.seq.|| is bounded_above;

        for n be Nat holds ( - 1) < ( ||.seq.|| . n)

        proof

          let n be Nat;

           ||.(seq . n).|| = ( ||.seq.|| . n) by NORMSP_0:def 4;

          hence thesis;

        end;

        then ||.seq.|| is bounded_below;

        then

        consider seq1 be sequence of X such that

         P1: seq1 is subsequence of seq & seq1 is weakly-convergent by AS, Th813, B5;

        ( w-lim seq1) in X;

        hence thesis by P1;

      end;

      hence thesis;

    end;