dualsp02.miz



    begin

    theorem :: DUALSP02:1

    

     Th63: for V be RealNormSpace, X be SubRealNormSpace of V, x0 be Point of V, d be Real st ex Z be non empty Subset of REAL st Z = { ||.(x - x0).|| where x be Point of V : x in X } & d = ( lower_bound Z) > 0 holds not x0 in X & ex G be Point of ( DualSp V) st (for x be Point of V st x in X holds (( Bound2Lipschitz (G,V)) . x) = 0 ) & (( Bound2Lipschitz (G,V)) . x0) = 1 & ||.G.|| = (1 / d)

    proof

      let V be RealNormSpace, X be SubRealNormSpace of V, x0 be Point of V, d be Real;

      assume ex Z be non empty Subset of REAL st Z = { ||.(x - x0).|| where x be Point of V : x in X } & d = ( lower_bound Z) > 0 ;

      then

      consider Z be non empty Subset of REAL such that

       AS2: Z = { ||.(x - x0).|| where x be Point of V : x in X } & d = ( lower_bound Z) > 0 ;

      set M0 = { (z + (a * x0)) where z be Point of V, a be Real : z in X };

      

       A1: ( 0. V) = (( 0. V) + ( 0 * x0)) by RLVECT_1: 10;

      ( 0. V) = ( 0. X) by DUALSP01:def 16;

      then

       D1: ( 0. V) in X;

      then ( 0. V) in M0 by A1;

      then

      reconsider M0 as non empty set;

      now

        let x be object;

        assume x in M0;

        then ex z be Point of V, a be Real st x = (z + (a * x0)) & z in X;

        hence x in the carrier of V;

      end;

      then M0 c= the carrier of V;

      then

      reconsider M0 as non empty Subset of V;

      

       B0: X is Subspace of V by NORMSP_3: 27;

      set M = ( NLin M0);

      

       AD1: M0 is linearly-closed

      proof

        

         A0: for v,u be VECTOR of V st v in M0 & u in M0 holds (v + u) in M0

        proof

          let v,u be VECTOR of V;

          assume

           A1: v in M0 & u in M0;

          then

          consider z1 be Point of V, a be Real such that

           A3: v = (z1 + (a * x0)) & z1 in X;

          consider z2 be Point of V, b be Real such that

           A5: u = (z2 + (b * x0)) & z2 in X by A1;

          

           A7: (v + u) = (z1 + ((a * x0) + (z2 + (b * x0)))) by A3, A5, RLVECT_1:def 3

          .= (z1 + (z2 + ((a * x0) + (b * x0)))) by RLVECT_1:def 3

          .= ((z1 + z2) + ((a * x0) + (b * x0))) by RLVECT_1:def 3

          .= ((z1 + z2) + ((a + b) * x0)) by RLVECT_1:def 6;

          (z1 + z2) in X by B0, A3, A5, RLSUB_1: 20;

          hence thesis by A7;

        end;

        for r be Real, v be VECTOR of V st v in M0 holds (r * v) in M0

        proof

          let r be Real;

          let v be VECTOR of V;

          assume v in M0;

          then

          consider z be Point of V, a be Real such that

           A9: v = (z + (a * x0)) & z in X;

          

           A11: (r * v) = ((r * z) + (r * (a * x0))) by A9, RLVECT_1:def 5

          .= ((r * z) + ((r * a) * x0)) by RLVECT_1:def 7;

          (r * z) in X by B0, A9, RLSUB_1: 21;

          hence thesis by A11;

        end;

        hence thesis by A0;

      end;

      then

       X01: the carrier of M = M0 by NORMSP_3: 31;

      

       V2: x0 = (( 0. V) + (1 * x0)) by RLVECT_1:def 8;

      then

       V21: x0 in M by D1, X01;

      

       AD2: for v be Point of M holds ex x be Point of V, a be Real st v = (x + (a * x0)) & x in X

      proof

        let v be Point of M;

        v in the carrier of ( Lin M0);

        then v in M0 by AD1, NORMSP_3: 31;

        hence thesis;

      end;

      reconsider r0 = 0 as Real;

      for r be ExtReal st r in Z holds r0 <= r

      proof

        let r be ExtReal;

        assume r in Z;

        then ex x be Point of V st r = ||.(x - x0).|| & x in X by AS2;

        hence r0 <= r;

      end;

      then r0 is LowerBound of Z by XXREAL_2:def 2;

      then

       U2: Z is bounded_below;

       P4:

      now

        assume

         Q1: x0 in X;

        reconsider x0 as Point of V;

         ||.(x0 - x0).|| = ||.( 0. V).|| by RLVECT_1: 15;

        then r0 in Z by Q1, AS2;

        hence contradiction by AS2, U2, SEQ_4:def 2;

      end;

      hence not x0 in X;

      

       AD3: for x1,x2 be Point of V, a1,a2 be Real st x1 in X & x2 in X & (x1 + (a1 * x0)) = (x2 + (a2 * x0)) holds x1 = x2 & a1 = a2

      proof

        let x1,x2 be Point of V, a1,a2 be Real;

        assume

         P1: x1 in X & x2 in X & (x1 + (a1 * x0)) = (x2 + (a2 * x0));

        

        then ((x1 + (a1 * x0)) - x2) = ((x2 + ( - x2)) + (a2 * x0)) by RLVECT_1:def 3

        .= (( 0. V) + (a2 * x0)) by RLVECT_1: 5;

        then

         P5: (((x1 + (a1 * x0)) - x2) - (a1 * x0)) = ((a2 - a1) * x0) by RLVECT_1: 35;

        

         P6: (((x1 + (a1 * x0)) - x2) - (a1 * x0)) = ((x1 + (a1 * x0)) + (( - x2) - (a1 * x0))) by RLVECT_1:def 3

        .= (x1 + ((a1 * x0) + (( - x2) - (a1 * x0)))) by RLVECT_1:def 3

        .= (x1 + (((a1 * x0) + ( - x2)) - (a1 * x0))) by RLVECT_1:def 3

        .= (x1 + (( - x2) + ((a1 * x0) - (a1 * x0)))) by RLVECT_1:def 3

        .= (x1 + (( - x2) + ( 0. V))) by RLVECT_1: 15;

        

         P7: a2 = a1

        proof

          assume a2 <> a1;

          then

           Q0: (a2 - a1) <> 0 ;

          then

           Q1: ((a2 - a1) * (1 / (a2 - a1))) = 1 by XCMPLX_1: 106;

          (1 * (x1 - x2)) = ((a2 - a1) * x0) by P5, P6, RLVECT_1:def 8;

          then ((a2 - a1) * ((1 / (a2 - a1)) * (x1 - x2))) = ((a2 - a1) * x0) by Q1, RLVECT_1:def 7;

          then

           Q2: ((1 / (a2 - a1)) * (x1 - x2)) = x0 by Q0, RLVECT_1: 36;

          reconsider r = (1 / (a2 - a1)) as Real;

          

           Q4: (r * x1) in X & (r * x2) in X by B0, P1, RLSUB_1: 21;

          (r * (x1 - x2)) = ((r * x1) - (r * x2)) by RLVECT_1: 34;

          hence contradiction by P4, Q2, B0, Q4, RLSUB_1: 23;

        end;

        then (x1 - x2) = ( 0. V) by P5, P6, RLVECT_1: 10;

        hence thesis by P7, RLVECT_1: 21;

      end;

      defpred P[ object, object] means ex z be Point of V, a be Real st z in X & $1 = (z + (a * x0)) & $2 = a;

      

       F1: for v be Element of M holds ex a be Element of REAL st P[v, a]

      proof

        let v be Element of M;

        consider z be Point of V, a be Real such that

         B0: v = (z + (a * x0)) & z in X by AD2;

        reconsider aa = a as Element of REAL by XREAL_0:def 1;

        take aa;

        thus thesis by B0;

      end;

      consider f be Function of M, REAL such that

       A1F: for x be Element of M holds P[x, (f . x)] from FUNCT_2:sch 3( F1);

      

       A1: for v be Point of M, z be Point of V, a be Real st z in X & v = (z + (a * x0)) holds (f . v) = a

      proof

        let v be Point of M, z be Point of V, a be Real;

        assume

         AS0: z in X & v = (z + (a * x0));

        ex z1 be Point of V, a1 be Real st z1 in X & v = (z1 + (a1 * x0)) & (f . v) = a1 by A1F;

        hence (f . v) = a by AS0, AD3;

      end;

      f is linear-Functional of M

      proof

        

         B1: f is additive

        proof

          let v,w be VECTOR of M;

          consider x1 be Point of V, a1 be Real such that

           B11: v = (x1 + (a1 * x0)) & x1 in X by AD2;

          consider x2 be Point of V, a2 be Real such that

           B13: w = (x2 + (a2 * x0)) & x2 in X by AD2;

          

           B14: (f . v) = a1 & (f . w) = a2 by A1, B11, B13;

          (v + w) = ((x1 + (a1 * x0)) + (x2 + (a2 * x0))) by B11, B13, NORMSP_3: 28

          .= (x1 + ((a1 * x0) + (x2 + (a2 * x0)))) by RLVECT_1:def 3

          .= (x1 + (x2 + ((a1 * x0) + (a2 * x0)))) by RLVECT_1:def 3

          .= ((x1 + x2) + ((a1 * x0) + (a2 * x0))) by RLVECT_1:def 3

          .= ((x1 + x2) + ((a1 + a2) * x0)) by RLVECT_1:def 6;

          hence (f . (v + w)) = ((f . v) + (f . w)) by B14, A1, B0, B11, B13, RLSUB_1: 20;

        end;

        f is homogeneous

        proof

          let v be VECTOR of M, r be Real;

          consider x be Point of V, a be Real such that

           B11: v = (x + (a * x0)) & x in X by AD2;

          (r * v) = (r * (x + (a * x0))) by B11, NORMSP_3: 28

          .= ((r * x) + (r * (a * x0))) by RLVECT_1:def 5

          .= ((r * x) + ((r * a) * x0)) by RLVECT_1:def 7;

          

          hence (f . (r * v)) = (r * a) by A1, B0, B11, RLSUB_1: 21

          .= (r * (f . v)) by A1, B11;

        end;

        hence thesis by B1;

      end;

      then

      reconsider f as linear-Functional of M;

      

       A5: for v be Point of M holds |.(f . v).| <= ((1 / d) * ||.v.||)

      proof

        let v be Point of M;

        consider x be Point of V, a be Real such that

         B5: v = (x + (a * x0)) & x in X by AD2;

        per cases ;

          suppose a = 0 ;

          then |.(f . (x + (a * x0))).| = 0 by A1, B5, ABSVALUE: 2;

          hence |.(f . v).| <= ((1 / d) * ||.v.||) by AS2, B5;

        end;

          suppose

           B6: a <> 0 ;

          

           C3: ||.(x + (a * x0)).|| = ||.((1 * x) + (a * x0)).|| by RLVECT_1:def 8

          .= ||.(((a * (1 / a)) * x) + (a * x0)).|| by B6, XCMPLX_1: 106

          .= ||.((a * ((1 / a) * x)) + (a * x0)).|| by RLVECT_1:def 7

          .= ||.(a * (((1 / a) * x) + x0)).|| by RLVECT_1:def 5

          .= ( |.a.| * ||.(((1 / a) * x) + x0).||) by NORMSP_1:def 1;

          

           C4: ||.(((1 / a) * x) + x0).|| = ||.( - (((1 / a) * x) + x0)).|| by NORMSP_1: 2

          .= ||.(( - ((1 / a) * x)) - x0).|| by RLVECT_1: 30;

          set s = ||.(( - ((1 / a) * x)) - x0).||;

          

           C52: ( - ((1 / a) * x)) = ((1 / a) * ( - x)) by RLVECT_1: 25;

          ( - x) in X by B0, B5, RLSUB_1: 22;

          then ( - ((1 / a) * x)) in X by B0, C52, RLSUB_1: 21;

          then s in Z by AS2;

          then

           C5: ||.(( - ((1 / a) * x)) - x0).|| >= d by AS2, U2, SEQ_4:def 2;

           |.a.| >= 0 by COMPLEX1: 46;

          then ( |.a.| * ||.(( - ((1 / a) * x)) - x0).||) >= ( |.a.| * d) by C5, XREAL_1: 64;

          then ( ||.(x + (a * x0)).|| / d) >= |.a.| by AS2, C3, C4, XREAL_1: 77;

          then ((1 / d) * ||.(x + (a * x0)).||) >= |.a.| by XCMPLX_1: 99;

          then |.(f . (x + (a * x0))).| <= ((1 / d) * ||.(x + (a * x0)).||) by A1, B5;

          hence |.(f . v).| <= ((1 / d) * ||.v.||) by B5, NORMSP_3: 28;

        end;

      end;

      then f is Lipschitzian by AS2;

      then

      reconsider f as Lipschitzian linear-Functional of M;

      reconsider F = f as Point of ( DualSp M) by DUALSP01:def 10;

      consider g be Lipschitzian linear-Functional of V, G be Point of ( DualSp V) such that

       C1: g = G & (g | the carrier of M) = f & ||.G.|| = ||.F.|| by DUALSP01: 36;

      

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

      proof

        let x be Point of V;

        assume

         A32: x in X;

        x = (x + ( 0. V));

        then

         A33: x = (x + ( 0 * x0)) by RLVECT_1: 10;

        then

         A34: x in M by X01, A32;

        

        thus (( Bound2Lipschitz (G,V)) . x) = (G . x) by SUBSET_1:def 8

        .= (f . x) by A34, C1, FUNCT_1: 49

        .= 0 by A33, A32, A34, A1;

      end;

      

       A12: (( Bound2Lipschitz (G,V)) . x0) = (G . x0) by SUBSET_1:def 8

      .= (f . x0) by C1, V21, FUNCT_1: 49

      .= 1 by A1, V2, D1, V21;

      take G;

      now

        let r be Real;

        assume r in ( PreNorms f);

        then

        consider t be VECTOR of M such that

         C1: r = |.(f . t).| & ||.t.|| <= 1;

        

         C3: |.(f . t).| <= ((1 / d) * ||.t.||) by A5;

        ((1 / d) * ||.t.||) <= ((1 / d) * 1) by AS2, C1, XREAL_1: 64;

        hence r <= (1 / d) by C1, C3, XXREAL_0: 2;

      end;

      then ( upper_bound ( PreNorms f)) <= (1 / d) by SEQ_4: 45;

      then

       B3: ||.F.|| <= (1 / d) by DUALSP01: 24;

      now

        let s be Real;

        assume 0 < s;

        then

        consider r be Real such that

         B32: r in Z & r < (( lower_bound Z) + s) by U2, SEQ_4:def 2;

        consider x be Point of V such that

         B34: r = ||.(x - x0).|| & x in X by B32, AS2;

        

         B35: (x - x0) = (x + (( - 1) * x0)) by RLVECT_1: 16;

        then (x - x0) in M0 by B34;

        then

        reconsider xx0 = (x - x0) as Point of M by AD1, NORMSP_3: 31;

         |.(f . xx0).| = |.( - 1).| by B35, A1, B34

        .= |.1.| by COMPLEX1: 52

        .= 1 by COMPLEX1: 43;

        then

         B38: 1 <= ( ||.F.|| * ||.xx0.||) by DUALSP01: 26;

         ||.xx0.|| = r by NORMSP_3: 28, B34;

        then ( ||.F.|| * ||.xx0.||) <= ( ||.F.|| * (d + s)) by AS2, B32, XREAL_1: 64;

        hence 1 <= (( ||.F.|| * d) + ( ||.F.|| * s)) by B38, XXREAL_0: 2;

      end;

      then 1 <= ( ||.F.|| * d) by NORMSP_3: 22;

      then (1 / d) <= (( ||.F.|| * d) / d) by XREAL_1: 72, AS2;

      then (1 / d) <= ||.F.|| by XCMPLX_1: 89, AS2;

      hence thesis by A31, A12, C1, B3, XXREAL_0: 1;

    end;

    theorem :: DUALSP02:2

    

     Lm64: for V be RealNormSpace, Y be non empty Subset of V, x0 be Point of V st Y is linearly-closed & Y is closed & not x0 in Y holds ex G be Point of ( DualSp V) st (for x be Point of V st x in Y holds (( Bound2Lipschitz (G,V)) . x) = 0 ) & (( Bound2Lipschitz (G,V)) . x0) = 1

    proof

      let V be RealNormSpace, Y be non empty Subset of V, x0 be Point of V;

      assume

       AS: Y is linearly-closed & Y is closed & not x0 in Y;

      set X = ( NLin Y);

      

       X1: the carrier of X = Y by NORMSP_3: 31, AS;

      set Z = { ||.(x - x0).|| where x be Point of V : x in X };

      X is Subspace of V by NORMSP_3: 27;

      then ( 0. V) in X by RLSUB_1: 17;

      then

       X2: ||.(( 0. V) - x0).|| in Z;

      now

        let z be object;

        assume z in Z;

        then ex x be Point of V st z = ||.(x - x0).|| & x in X;

        hence z in REAL ;

      end;

      then Z c= REAL ;

      then

      reconsider Z as non empty Subset of REAL by X2;

      reconsider r0 = 0 as Real;

      for r be ExtReal st r in Z holds r0 <= r

      proof

        let r be ExtReal;

        assume r in Z;

        then ex x be Point of V st r = ||.(x - x0).|| & x in X;

        hence r0 <= r;

      end;

      then

       U1: r0 is LowerBound of Z by XXREAL_2:def 2;

      then Z is bounded_below;

      then

      reconsider Z as non empty bounded_below real-membered Subset of REAL ;

      reconsider d = ( lower_bound Z) as Real;

      

       X3: r0 <= ( inf Z) by U1, XXREAL_2:def 4;

      d > 0

      proof

        assume not d > 0 ;

        then

         X22: d = 0 by X3;

        reconsider Yt = (Y ` ) as Subset of ( TopSpaceNorm V);

        

         Z24: Yt is open by AS, NORMSP_2: 16;

        x0 in (the carrier of V \ Y) by AS, XBOOLE_0:def 5;

        then x0 in Yt by SUBSET_1:def 4;

        then

        consider s be Real such that

         X23: 0 < s & { y where y be Point of V : ||.(x0 - y).|| < s } c= Yt by Z24, NORMSP_2: 7;

        consider r be Real such that

         X24: r in Z & r < ( 0 + s) by X22, X23, SEQ_4:def 2;

        consider x be Point of V such that

         X25: r = ||.(x - x0).|| & x in X by X24;

         ||.(x0 - x).|| < s by X24, X25, NORMSP_1: 7;

        then x in { x where x be Point of V : ||.(x0 - x).|| < s };

        then x in Yt by X23;

        then x in (the carrier of V \ Y) by SUBSET_1:def 4;

        hence contradiction by X1, X25, XBOOLE_0:def 5;

      end;

      then

      consider G be Point of ( DualSp V) such that

       X3: (for x be Point of V st x in X holds (( Bound2Lipschitz (G,V)) . x) = 0 ) & (( Bound2Lipschitz (G,V)) . x0) = 1 & ||.G.|| = (1 / d) by Th63;

      take G;

      now

        let x be Point of V;

        assume x in Y;

        then x in X by NORMSP_3: 31, AS;

        hence (( Bound2Lipschitz (G,V)) . x) = 0 by X3;

      end;

      hence thesis by X3;

    end;

    theorem :: DUALSP02:3

    

     Lm65a: for V be RealNormSpace, x0 be Point of V st x0 <> ( 0. V) holds ex G be Point of ( DualSp V) st (( Bound2Lipschitz (G,V)) . x0) = 1 & ||.G.|| = (1 / ||.x0.||)

    proof

      let V be RealNormSpace, x0 be Point of V;

      assume

       AS0: x0 <> ( 0. V);

      set X = ( NLin {( 0. V)});

      set Y = the carrier of ( Lin {( 0. V)});

      for s be object holds s in Y iff s in {( 0. V)}

      proof

        let s be object;

        hereby

          assume s in Y;

          then s in ( Lin {( 0. V)});

          then ex a be Real st s = (a * ( 0. V)) by RLVECT_4: 8;

          hence s in {( 0. V)} by TARSKI:def 1;

        end;

        assume s in {( 0. V)};

        then s = (1 * ( 0. V)) by TARSKI:def 1;

        then s in ( Lin {( 0. V)}) by RLVECT_4: 8;

        hence s in Y;

      end;

      then

       Y1: the carrier of X = {( 0. V)} by TARSKI: 2;

      set Z = { ||.(x - x0).|| where x be Point of V : x in X };

      

       Y2: for s be object holds s in Z iff s in { ||.x0.||}

      proof

        let s be object;

        hereby

          assume s in Z;

          then

          consider x be Point of V such that

           Y11: s = ||.(x - x0).|| & x in X;

          x = ( 0. V) by Y1, Y11, TARSKI:def 1;

          then ||.(x - x0).|| = ||.x0.|| by NORMSP_1: 2;

          hence s in { ||.x0.||} by TARSKI:def 1, Y11;

        end;

        assume s in { ||.x0.||};

        then s = ||.x0.|| by TARSKI:def 1;

        then

         X1: s = ||.(( 0. V) - x0).|| by NORMSP_1: 2;

        ( 0. V) in X by Y1, TARSKI:def 1;

        hence s in Z by X1;

      end;

      then

      reconsider Z as non empty Subset of REAL by TARSKI: 2;

      reconsider d = ( lower_bound Z) as Real;

      

       Y3: Z = { ||.x0.||} by Y2;

      then

       X4: d = ||.x0.|| by SEQ_4: 9;

      then d <> 0 by AS0, NORMSP_0:def 5;

      then

      consider G be Point of ( DualSp V) such that

       X3: (for x be Point of V st x in X holds (( Bound2Lipschitz (G,V)) . x) = 0 ) & (( Bound2Lipschitz (G,V)) . x0) = 1 & ||.G.|| = (1 / d) by X4, Th63;

      take G;

      thus thesis by X3, SEQ_4: 9, Y3;

    end;

    theorem :: DUALSP02:4

    

     Lm65: for V be RealNormSpace, x0 be Point of V st x0 <> ( 0. V) holds ex F be Point of ( DualSp V) st ||.F.|| = 1 & (( Bound2Lipschitz (F,V)) . x0) = ||.x0.||

    proof

      let V be RealNormSpace, x0 be Point of V;

      assume

       AS: x0 <> ( 0. V);

      then

      consider G be Point of ( DualSp V) such that

       A2: (( Bound2Lipschitz (G,V)) . x0) = 1 & ||.G.|| = (1 / ||.x0.||) by Lm65a;

      reconsider d = ||.x0.|| as Real;

      reconsider F = (d * G) as Point of ( DualSp V);

      take F;

      

       A4: ||.F.|| = ( |.d.| * ||.G.||) by NORMSP_1:def 1

      .= (d * (1 / d)) by A2, ABSVALUE:def 1

      .= 1 by AS, NORMSP_0:def 5, XCMPLX_1: 106;

      (( Bound2Lipschitz (F,V)) . x0) = (d * (G . x0)) by DUALSP01: 30, SUBSET_1:def 8

      .= (d * (( Bound2Lipschitz (G,V)) . x0)) by SUBSET_1:def 8;

      hence thesis by A2, A4;

    end;

    theorem :: DUALSP02:5

    

     Lm65A: for V be RealNormSpace st V is non trivial holds ex F be Point of ( DualSp V) st ||.F.|| = 1

    proof

      let V be RealNormSpace;

      assume V is non trivial;

      then

      consider x0 be Element of V such that

       P1: x0 <> ( 0. V);

      ex F be Point of ( DualSp V) st ||.F.|| = 1 & (( Bound2Lipschitz (F,V)) . x0) = ||.x0.|| by Lm65, P1;

      hence thesis;

    end;

    theorem :: DUALSP02:6

    

     Lm65A1: for V be RealNormSpace st V is non trivial holds ( DualSp V) is non trivial

    proof

      let V be RealNormSpace;

      assume V is non trivial;

      then

      consider F be Point of ( DualSp V) such that

       A1: ||.F.|| = 1 by Lm65A;

      F <> ( 0. ( DualSp V)) by A1;

      hence thesis;

    end;

    begin

    theorem :: DUALSP02:7

    

     Th71: for V be RealNormSpace, x be Point of V st V is non trivial holds (ex X be non empty Subset of REAL st X = { |.(( Bound2Lipschitz (F,V)) . x).| where F be Point of ( DualSp V) : ||.F.|| = 1 } & ||.x.|| = ( upper_bound X)) & (ex Y be non empty Subset of REAL st Y = { |.(( Bound2Lipschitz (F,V)) . x).| where F be Point of ( DualSp V) : ||.F.|| <= 1 } & ||.x.|| = ( upper_bound Y))

    proof

      let V be RealNormSpace, x be Point of V;

      assume

       AS: V is non trivial;

      set X = { |.(( Bound2Lipschitz (F,V)) . x).| where F be Point of ( DualSp V) : ||.F.|| = 1 };

      set Y = { |.(( Bound2Lipschitz (F,V)) . x).| where F be Point of ( DualSp V) : ||.F.|| <= 1 };

      consider F0 be Point of ( DualSp V) such that

       P1: ||.F0.|| = 1 by AS, Lm65A;

      

       P2: |.(( Bound2Lipschitz (F0,V)) . x).| in X & |.(( Bound2Lipschitz (F0,V)) . x).| in Y by P1;

      

       P3: X c= Y

      proof

        let z be object;

        assume z in X;

        then ex F be Point of ( DualSp V) st z = |.(( Bound2Lipschitz (F,V)) . x).| & ||.F.|| = 1;

        hence z in Y;

      end;

      

       P4: Y c= REAL

      proof

        let z be object;

        assume z in Y;

        then ex F be Point of ( DualSp V) st z = |.(( Bound2Lipschitz (F,V)) . x).| & ||.F.|| <= 1;

        hence z in REAL by XREAL_0:def 1;

      end;

      then

      reconsider Y as non empty Subset of REAL by P2;

      X c= REAL by P3, P4;

      then

      reconsider X as non empty Subset of REAL by P2;

      per cases ;

        suppose

         X1: x = ( 0. V);

        for t be object st t in Y holds t in { 0 qua Real}

        proof

          let t be object;

          assume t in Y;

          then ex F be Point of ( DualSp V) st t = |.(( Bound2Lipschitz (F,V)) . x).| & ||.F.|| <= 1;

          then t = 0 by ABSVALUE: 2, X1, HAHNBAN: 20;

          hence t in { 0 qua Real} by TARSKI:def 1;

        end;

        then

         P6: Y c= { 0 qua Real} & X c= { 0 qua Real} by P3;

        ex z be object st z in X by XBOOLE_0:def 1;

        then 0 in X by P6, TARSKI:def 1;

        then X = { 0 qua Real} & Y = { 0 qua Real} by P6, P3, ZFMISC_1: 31;

        then ( upper_bound X) = 0 & ( upper_bound Y) = 0 by SEQ_4: 9;

        then ||.x.|| = ( upper_bound X) & ||.x.|| = ( upper_bound Y) by X1;

        hence thesis;

      end;

        suppose

         Z1: x <> ( 0. V);

        

         X6: for r be ExtReal st r in Y holds r <= ||.x.||

        proof

          let r be ExtReal;

          assume r in Y;

          then

          consider F be Point of ( DualSp V) such that

           X4: r = |.(( Bound2Lipschitz (F,V)) . x).| & ||.F.|| <= 1;

          

           X5: |.(( Bound2Lipschitz (F,V)) . x).| <= ( ||.F.|| * ||.x.||) by DUALSP01: 26, SUBSET_1:def 8;

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

          hence r <= ||.x.|| by X4, X5, XXREAL_0: 2;

        end;

        then ||.x.|| is UpperBound of Y by XXREAL_2:def 1;

        then

         X7: Y is bounded_above;

        then

         X8: ( upper_bound X) <= ( upper_bound Y) by P3, SEQ_4: 48;

        for r be Real st r in Y holds r <= ||.x.|| by X6;

        then

         X9: ( upper_bound Y) <= ||.x.|| by SEQ_4: 45;

        then

         X10: ( upper_bound X) <= ||.x.|| by X8, XXREAL_0: 2;

        consider F0 be Point of ( DualSp V) such that

         Y1: ||.F0.|| = 1 & (( Bound2Lipschitz (F0,V)) . x) = ||.x.|| by Lm65, Z1;

         |.(( Bound2Lipschitz (F0,V)) . x).| = ||.x.|| by Y1, ABSVALUE:def 1;

        then

         Y3: ||.x.|| in X by Y1;

        X is bounded_above by P3, X7, XXREAL_2: 43;

        then ||.x.|| <= ( upper_bound X) by Y3, SEQ_4:def 1;

        then ||.x.|| = ( upper_bound X) by X10, XXREAL_0: 1;

        hence thesis by X9, X8, XXREAL_0: 1;

      end;

    end;

    theorem :: DUALSP02:8

    

     Lm72: for V be RealNormSpace, x be Point of V st for f be Lipschitzian linear-Functional of V holds (f . x) = 0 holds x = ( 0. V)

    proof

      let V be RealNormSpace, x be Point of V;

      assume

       AS: for f be Lipschitzian linear-Functional of V holds (f . x) = 0 ;

      assume x <> ( 0. V);

      then ex G be Point of ( DualSp V) st (( Bound2Lipschitz (G,V)) . x) = 1 & ||.G.|| = (1 / ||.x.||) by Lm65a;

      hence contradiction by AS;

    end;

    definition

      let X be RealNormSpace;

      let x be Point of X;

      :: DUALSP02:def1

      func BiDual x -> Point of ( DualSp ( DualSp X)) means

      : Def1: for f be Point of ( DualSp X) holds (it . f) = (f . x);

      existence

      proof

        deffunc F( Element of ( DualSp X)) = ($1 . x);

        

         P0: ex f be Function of the carrier of ( DualSp X), REAL st for fai be Element of ( DualSp X) holds (f . fai) = F(fai) from FUNCT_2:sch 4;

        consider f be Function of the carrier of ( DualSp X), REAL such that

         P1: for fai be Point of ( DualSp X) holds (f . fai) = (fai . x) by P0;

        

         P2: f is additive

        proof

          let y,z be Point of ( DualSp X);

          (f . (y + z)) = ((y + z) . x) by P1

          .= ((y . x) + (z . x)) by DUALSP01: 29

          .= ((f . y) + (z . x)) by P1;

          hence (f . (y + z)) = ((f . y) + (f . z)) by P1;

        end;

        

         P3: f is homogeneous

        proof

          let y be Point of ( DualSp X), r be Real;

          (f . (r * y)) = ((r * y) . x) by P1

          .= (r * (y . x)) by DUALSP01: 30;

          hence (f . (r * y)) = (r * (f . y)) by P1;

        end;

        for y be Point of ( DualSp X) holds |.(f . y).| <= ( ||.x.|| * ||.y.||)

        proof

          let y be Point of ( DualSp X);

          reconsider y1 = y as Lipschitzian linear-Functional of X by DUALSP01:def 10;

           |.(y1 . x).| <= ( ||.y.|| * ||.x.||) by DUALSP01: 26;

          hence thesis by P1;

        end;

        then f is Lipschitzian;

        then

        reconsider f as Point of ( DualSp ( DualSp X)) by P2, P3, DUALSP01:def 10;

        take f;

        thus thesis by P1;

      end;

      uniqueness

      proof

        let F1,F2 be Point of ( DualSp ( DualSp X));

        assume

         A1: (for f be Point of ( DualSp X) holds (F1 . f) = (f . x)) & (for f be Point of ( DualSp X) holds (F2 . f) = (f . x));

        

         A2: F1 is Lipschitzian linear-Functional of ( DualSp X) & F2 is Lipschitzian linear-Functional of ( DualSp X) by DUALSP01:def 10;

        then

         A3: ( dom F1) = the carrier of ( DualSp X) & ( dom F2) = the carrier of ( DualSp X) by FUNCT_2:def 1;

        now

          let f be object;

          assume f in ( dom F1);

          then

          reconsider f1 = f as Point of ( DualSp X) by A2, FUNCT_2:def 1;

          (F1 . f) = (f1 . x) by A1;

          hence (F1 . f) = (F2 . f) by A1;

        end;

        hence F1 = F2 by A3;

      end;

    end

    definition

      let X be RealNormSpace;

      :: DUALSP02:def2

      func BidualFunc X -> Function of X, ( DualSp ( DualSp X)) means

      : Def2: for x be Point of X holds (it . x) = ( BiDual x);

      existence

      proof

        deffunc F( Element of X) = ( BiDual $1);

        ex f be Function of X, ( DualSp ( DualSp X)) st for x be Element of the carrier of X holds (f . x) = F(x) from FUNCT_2:sch 4;

        then

        consider f be Function of X, ( DualSp ( DualSp X)) such that

         P1: for x be Point of X holds (f . x) = ( BiDual x);

        take f;

        thus thesis by P1;

      end;

      uniqueness

      proof

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

        assume

         A1: (for x be Point of X holds (f1 . x) = ( BiDual x)) & (for x be Point of X holds (f2 . x) = ( BiDual x));

        

         A3: ( dom f1) = the carrier of X & ( dom f2) = the carrier of X by FUNCT_2:def 1;

        now

          let x be object;

          assume x in ( dom f1);

          then

          reconsider x1 = x as Point of X;

          (f1 . x) = ( BiDual x1) by A1;

          hence (f1 . x) = (f2 . x) by A1;

        end;

        hence f1 = f2 by A3;

      end;

    end

    registration

      let X be RealNormSpace;

      cluster ( BidualFunc X) -> additive homogeneous;

      coherence

      proof

        reconsider f = ( BidualFunc X) as Function of X, ( DualSp ( DualSp X));

        

         A0: f is additive

        proof

          let x,y be Point of X;

          

           A1: (f . (x + y)) is Function of the carrier of ( DualSp X), REAL & ((f . x) + (f . y)) is Function of the carrier of ( DualSp X), REAL by DUALSP01:def 10;

          for g be Point of ( DualSp X) holds ((f . (x + y)) . g) = (((f . x) + (f . y)) . g)

          proof

            let g be Point of ( DualSp X);

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

            

            thus ((f . (x + y)) . g) = (( BiDual (x + y)) . g) by Def2

            .= (g . (x + y)) by Def1

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

            .= ((( BiDual x) . g) + (g . y)) by Def1

            .= ((( BiDual x) . g) + (( BiDual y) . g)) by Def1

            .= (((f . x) . g) + (( BiDual y) . g)) by Def2

            .= (((f . x) . g) + ((f . y) . g)) by Def2

            .= (((f . x) + (f . y)) . g) by DUALSP01: 29;

          end;

          hence (f . (x + y)) = ((f . x) + (f . y)) by A1, FUNCT_2:def 8;

        end;

        f is homogeneous

        proof

          let x be Point of X, r be Real;

          

           A3: (f . (r * x)) is Function of the carrier of ( DualSp X), REAL & (r * (f . x)) is Function of the carrier of ( DualSp X), REAL by DUALSP01:def 10;

          for g be Point of ( DualSp X) holds ((f . (r * x)) . g) = ((r * (f . x)) . g)

          proof

            let g be Point of ( DualSp X);

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

            

            thus ((f . (r * x)) . g) = (( BiDual (r * x)) . g) by Def2

            .= (g . (r * x)) by Def1

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

            .= (r * (( BiDual x) . g)) by Def1

            .= (r * ((f . x) . g)) by Def2

            .= ((r * (f . x)) . g) by DUALSP01: 30;

          end;

          hence (f . (r * x)) = (r * (f . x)) by A3, FUNCT_2:def 8;

        end;

        hence thesis by A0;

      end;

    end

    registration

      let X be RealNormSpace;

      cluster ( BidualFunc X) -> one-to-one;

      coherence

      proof

        reconsider f = ( BidualFunc X) as Function of X, ( DualSp ( DualSp X));

        

         A0: f is additive homogeneous;

        for x1,x2 be object st x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2) holds x1 = x2

        proof

          let x1,x2 be object;

          assume

           A1: x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

          then

          reconsider y1 = x1, y2 = x2 as Point of X;

          

           A3: (f . (y1 - y2)) = ( BiDual (y1 - y2)) by Def2;

          (y1 - y2) = (y1 + (( - 1) * y2)) by RLVECT_1: 16;

          then

           A5: (f . (y1 - y2)) = ((f . y1) + (f . (( - 1) * y2))) by A0;

          (f . (( - 1) * y2)) = (( - 1) * (f . y2)) by LOPBAN_1:def 5;

          then (f . (y1 - y2)) = ((f . y1) - (f . y2)) by A5, RLVECT_1: 16;

          then

           A7: ( BiDual (y1 - y2)) = ( 0. ( DualSp ( DualSp X))) by A3, A1, RLVECT_1: 15;

          for g be Lipschitzian linear-Functional of X holds (g . (y1 - y2)) = 0

          proof

            let g be Lipschitzian linear-Functional of X;

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

            

             A8: (( BiDual (y1 - y2)) . g1) = (g1 . (y1 - y2)) by Def1;

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

            hence (g . (y1 - y2)) = 0 by A7, A8, FUNCOP_1: 7;

          end;

          then (y1 - y2) = ( 0. X) by Lm72;

          hence x1 = x2 by RLVECT_1: 21;

        end;

        hence thesis;

      end;

    end

    

     LMNORM: for X be RealNormSpace, x be Point of X st X is non trivial holds ||.x.|| = ||.(( BidualFunc X) . x).||

    proof

      let X be RealNormSpace, x be Point of X;

      assume

       AS: X is non trivial;

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

      consider Y be non empty Subset of REAL such that

       A1: Y = { |.(( Bound2Lipschitz (s,X)) . x).| where s be Point of ( DualSp X) : ||.s.|| <= 1 } & ||.x.|| = ( upper_bound Y) by AS, Th71;

      set Z = { |.(f . t).| where t be Point of ( DualSp X) : ||.t.|| <= 1 };

      

       A2: Y c= Z

      proof

        let y be object;

        assume y in Y;

        then

        consider s be Point of ( DualSp X) such that

         B1: y = |.(( Bound2Lipschitz (s,X)) . x).| & ||.s.|| <= 1 by A1;

        s is Lipschitzian linear-Functional of X by DUALSP01:def 10;

        then

         B2: |.(( Bound2Lipschitz (s,X)) . x).| = |.(s . x).| by DUALSP01: 23;

        (f . s) = (s . x) by Def1;

        hence y in Z by B1, B2;

      end;

      ( upper_bound Y) <= ( upper_bound ( PreNorms f)) by A2, SEQ_4: 48;

      then

       A4: ||.x.|| <= ||.( BiDual x).|| by A1, DUALSP01: 24;

      Z c= Y

      proof

        let y be object;

        assume y in Z;

        then

        consider t be Point of ( DualSp X) such that

         C1: y = |.(f . t).| & ||.t.|| <= 1;

        t is Lipschitzian linear-Functional of X by DUALSP01:def 10;

        then

         C2: |.(( Bound2Lipschitz (t,X)) . x).| = |.(t . x).| by DUALSP01: 23;

         |.(f . t).| = |.(t . x).| by Def1;

        hence y in Y by C1, C2, A1;

      end;

      then Y = Z by A2;

      then ( upper_bound ( PreNorms f)) <= ( upper_bound Y);

      then ||.( BiDual x).|| <= ( upper_bound Y) by DUALSP01: 24;

      then ||.( BiDual x).|| = ||.x.|| by A1, A4, XXREAL_0: 1;

      hence thesis by Def2;

    end;

    theorem :: DUALSP02:9

    for X be RealNormSpace st X is non trivial holds ( BidualFunc X) is LinearOperator of X, ( DualSp ( DualSp X)) & for x be Point of X holds ||.x.|| = ||.(( BidualFunc X) . x).|| by LMNORM;

    theorem :: DUALSP02:10

    

     IMDDX: for X be RealNormSpace st X is non trivial holds ex DuX be SubRealNormSpace of ( DualSp ( DualSp X)), L be Lipschitzian LinearOperator of X, DuX st L is bijective & DuX = ( Im ( BidualFunc X)) & (for x be Point of X holds (L . x) = ( BiDual x)) & for x be Point of X holds ||.x.|| = ||.(L . x).||

    proof

      let X be RealNormSpace;

      assume

       A0: X is non trivial;

      set F = ( BidualFunc X);

      set V1 = ( rng F);

      

       D0: V1 is linearly-closed by NORMSP_3: 35;

      V1 <> {}

      proof

        assume V1 = {} ;

        then ( dom F) = {} by RELAT_1: 42;

        hence thesis by FUNCT_2:def 1;

      end;

      then the carrier of ( Lin V1) = V1 by NORMSP_3: 31, D0;

      then

       C4: the carrier of ( Im F) = ( rng F);

      then

      reconsider L = ( BidualFunc X) as Function of X, ( Im F) by FUNCT_2: 6;

      

       A3: F is additive homogeneous;

      

       B0: L is additive

      proof

        let x,y be Point of X;

        (L . (x + y)) = ((F . x) + (F . y)) by A3;

        hence (L . (x + y)) = ((L . x) + (L . y)) by NORMSP_3: 28;

      end;

      L is homogeneous

      proof

        let x be Point of X, r be Real;

        (L . (r * x)) = (r * (F . x)) by LOPBAN_1:def 5;

        hence (L . (r * x)) = (r * (L . x)) by NORMSP_3: 28;

      end;

      then

      reconsider L as LinearOperator of X, ( Im F) by B0;

      

       P5: for x be Point of X holds ||.x.|| = ||.(L . x).||

      proof

        let x be Point of X;

         ||.x.|| = ||.(( BidualFunc X) . x).|| by A0, LMNORM;

        hence thesis by NORMSP_3: 28;

      end;

      then for x be Point of X holds ||.(L . x).|| <= (1 * ||.x.||);

      then

      reconsider L as Lipschitzian LinearOperator of X, ( Im ( BidualFunc X)) by LOPBAN_1:def 8;

      take ( Im ( BidualFunc X)), L;

      L is one-to-one onto by C4;

      hence thesis by Def2, P5;

    end;

    begin

    definition

      :: DUALSP02:def3

      func RNS_Real -> RealNormSpace equals NORMSTR (# REAL , ( In ( 0 , REAL )), addreal , multreal , absreal #);

      coherence

      proof

        set T = NORMSTR (# REAL , ( In ( 0 , REAL )), addreal , multreal , absreal #);

        reconsider T as non empty NORMSTR;

        now

          let v,w be Element of T;

          reconsider v1 = v, w1 = w as Element of REAL ;

          

          thus (v + w) = (v1 + w1) by BINOP_2:def 9

          .= (w + v) by BINOP_2:def 9;

        end;

        then

         A1: T is Abelian;

        now

          let u,v,w be Element of T;

          reconsider u1 = u, v1 = v, w1 = w as Element of REAL ;

          

           B1: ( addreal . (u,v)) = (u1 + v1) & ( addreal . (v,w)) = (v1 + w1) by BINOP_2:def 9;

          

          thus ((u + v) + w) = ((u1 + v1) + w1) by B1, BINOP_2:def 9

          .= (u1 + (v1 + w1))

          .= (u + (v + w)) by B1, BINOP_2:def 9;

        end;

        then

         A2: T is add-associative;

        now

          let v be Element of T;

          reconsider v1 = v as Element of REAL ;

          

          thus (v + ( 0. T)) = (v1 + 0 ) by BINOP_2:def 9

          .= v;

        end;

        then

         A3: T is right_zeroed;

        

         A4: T is right_complementable

        proof

          let v be Element of T;

          reconsider v1 = v as Element of REAL ;

          reconsider w1 = ( - v1) as Element of REAL ;

          reconsider w = w1 as Element of T;

          take w;

          

          thus (v + w) = (v1 + w1) by BINOP_2:def 9

          .= ( 0. T);

        end;

        now

          let a,b be Real, v be Element of T;

          reconsider v1 = v as Element of REAL ;

          

           B1: ( multreal . (a,v)) = (a * v1) & ( multreal . (b,v)) = (b * v1) by BINOP_2:def 11;

          

          thus ((a + b) * v) = ((a + b) * v1) by BINOP_2:def 11

          .= ((v1 * a) + (v1 * b))

          .= ((a * v) + (b * v)) by B1, BINOP_2:def 9;

        end;

        then

         A5: T is scalar-distributive;

        now

          let a be Real, v,w be Element of T;

          reconsider v1 = v, w1 = w as Element of REAL ;

          

           B1: ( addreal . (v,w)) = (v1 + w1) by BINOP_2:def 9;

          

           B2: ( multreal . (a,v)) = (a * v1) & ( multreal . (a,w)) = (a * w1) by BINOP_2:def 11;

          

          thus (a * (v + w)) = (a * (v1 + w1)) by B1, BINOP_2:def 11

          .= ((a * v1) + (a * w1))

          .= ((a * v) + (a * w)) by B2, BINOP_2:def 9;

        end;

        then

         A6: T is vector-distributive;

        now

          let a,b be Real, v be Element of T;

          reconsider v1 = v as Element of REAL ;

          

           B1: ( multreal . (b,v)) = (b * v1) by BINOP_2:def 11;

          

          thus ((a * b) * v) = ((a * b) * v1) by BINOP_2:def 11

          .= (a * (b * v1))

          .= (a * (b * v)) by B1, BINOP_2:def 11;

        end;

        then

         A7: T is scalar-associative;

        now

          let v be Element of T;

          reconsider v1 = v as Element of REAL ;

          

          thus (1 * v) = (1 * v1) by BINOP_2:def 11

          .= v;

        end;

        then

         A8: T is scalar-unital;

        

         A9: T is reflexive by EUCLID:def 2, COMPLEX1: 44;

        now

          let v be Element of T;

          assume

           AS: ||.v.|| = 0 ;

          reconsider v1 = v as Element of REAL ;

           |.v1.| = 0 by AS, EUCLID:def 2;

          hence v = ( 0. T) by COMPLEX1: 45;

        end;

        then

         A10: T is discerning;

        now

          let a be Real, v,w be Element of T;

          reconsider v1 = v, w1 = w as Element of REAL ;

          (the normF of T . (a * v)) = ( absreal . (a * v1)) by BINOP_2:def 11;

          

          hence ||.(a * v).|| = |.(a * v1).| by EUCLID:def 2

          .= ( |.a.| * |.v1.|) by COMPLEX1: 65

          .= ( |.a.| * ||.v.||) by EUCLID:def 2;

          (the normF of T . (v + w)) = ( absreal . (v1 + w1)) by BINOP_2:def 9;

          then

           C3: ||.(v + w).|| = |.(v1 + w1).| by EUCLID:def 2;

          ( ||.v.|| + ||.w.||) = ( |.v1.| + ( absreal . w1)) by EUCLID:def 2

          .= ( |.v1.| + |.w1.|) by EUCLID:def 2;

          hence ||.(v + w).|| <= ( ||.v.|| + ||.w.||) by C3, COMPLEX1: 56;

        end;

        then T is RealNormSpace-like;

        hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10;

      end;

    end

    theorem :: DUALSP02:11

    for X be RealNormSpace, x be Element of REAL , v be Point of RNS_Real st x = v holds ( - x) = ( - v)

    proof

      let X be RealNormSpace, x be Element of REAL , v be Point of RNS_Real ;

      assume x = v;

      then (( - 1) * x) = (( - 1) * v) by BINOP_2:def 11;

      hence thesis by RLVECT_1: 16;

    end;

    theorem :: DUALSP02:12

    

     LMN6: for X be RealNormSpace, x be object holds x is additive homogeneous Function of X, REAL iff x is additive homogeneous Function of X, RNS_Real

    proof

      let X be RealNormSpace, x be object;

      hereby

        assume

         A1: x is additive homogeneous Function of X, REAL ;

        then

        reconsider f = x as linear-Functional of X;

        reconsider g = x as Function of X, RNS_Real by A1;

        

         A2: for v,w be Element of X holds (g . (v + w)) = ((g . v) + (g . w))

        proof

          let v,w be Element of X;

          

          thus (g . (v + w)) = ((f . v) + (f . w)) by HAHNBAN:def 2

          .= ((g . v) + (g . w)) by BINOP_2:def 9;

        end;

        for v be VECTOR of X, r be Real holds (g . (r * v)) = (r * (g . v))

        proof

          let v be VECTOR of X, r be Real;

          

          thus (g . (r * v)) = (r * (f . v)) by HAHNBAN:def 3

          .= (r * (g . v)) by BINOP_2:def 11;

        end;

        then g is additive homogeneous by LOPBAN_1:def 5, A2;

        hence x is additive homogeneous Function of X, RNS_Real ;

      end;

      assume

       B1: x is additive homogeneous Function of X, RNS_Real ;

      then

      reconsider g = x as additive homogeneous Function of X, RNS_Real ;

      reconsider f = x as Function of X, REAL by B1;

      

       B2: for v,w be Element of X holds (f . (v + w)) = ((f . v) + (f . w))

      proof

        let v,w be Element of X;

        

        thus (f . (v + w)) = ((g . v) + (g . w)) by VECTSP_1:def 20

        .= ((f . v) + (f . w)) by BINOP_2:def 9;

      end;

      for v be VECTOR of X, r be Real holds (f . (r * v)) = (r * (f . v))

      proof

        let v be VECTOR of X, r be Real;

        

        thus (f . (r * v)) = (r * (g . v)) by LOPBAN_1:def 5

        .= (r * (f . v)) by BINOP_2:def 11;

      end;

      hence thesis by B2, HAHNBAN:def 2, HAHNBAN:def 3;

    end;

    theorem :: DUALSP02:13

    

     LMN7: for X be RealNormSpace, x be object holds x is Lipschitzian additive homogeneous Function of X, REAL iff x is Lipschitzian additive homogeneous Function of X, RNS_Real

    proof

      let X be RealNormSpace, x be object;

      hereby

        assume

         A1: x is Lipschitzian additive homogeneous Function of X, REAL ;

        then

        reconsider f = x as Lipschitzian linear-Functional of X;

        reconsider g = x as additive homogeneous Function of X, RNS_Real by A1, LMN6;

        consider K be Real such that

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

        for v be VECTOR of X holds ||.(g . v).|| <= (K * ||.v.||)

        proof

          let v be VECTOR of X;

           |.(f . v).| <= (K * ||.v.||) by X1;

          hence ||.(g . v).|| <= (K * ||.v.||) by EUCLID:def 2;

        end;

        hence x is Lipschitzian additive homogeneous Function of X, RNS_Real by X1, LOPBAN_1:def 8;

      end;

      assume

       B1: x is Lipschitzian additive homogeneous Function of X, RNS_Real ;

      then

      reconsider g = x as Lipschitzian additive homogeneous Function of X, RNS_Real ;

      reconsider f = x as additive homogeneous Function of X, REAL by LMN6, B1;

      consider K be Real such that

       X1: 0 <= K & for v be VECTOR of X holds ||.(g . v).|| <= (K * ||.v.||) by LOPBAN_1:def 8;

      for v be VECTOR of X holds |.(f . v).| <= (K * ||.v.||)

      proof

        let v be VECTOR of X;

         ||.(g . v).|| <= (K * ||.v.||) by X1;

        hence |.(f . v).| <= (K * ||.v.||) by EUCLID:def 2;

      end;

      then f is Lipschitzian additive homogeneous by X1;

      hence x is Lipschitzian additive homogeneous Function of X, REAL ;

    end;

    theorem :: DUALSP02:14

    

     Th75A: for X be RealNormSpace holds the carrier of ( DualSp X) = the carrier of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ))

    proof

      let X be RealNormSpace;

      

       A1: for x be object holds x in ( BoundedLinearFunctionals X) iff x in ( BoundedLinearOperators (X, RNS_Real ))

      proof

        let x be object;

        hereby

          assume x in ( BoundedLinearFunctionals X);

          then x is Lipschitzian additive homogeneous Functional of X by DUALSP01:def 10;

          then x is Lipschitzian additive homogeneous Function of X, RNS_Real by LMN7;

          hence x in ( BoundedLinearOperators (X, RNS_Real )) by LOPBAN_1:def 9;

        end;

        assume x in ( BoundedLinearOperators (X, RNS_Real ));

        then x is Lipschitzian LinearOperator of X, RNS_Real by LOPBAN_1:def 9;

        then x is Lipschitzian additive homogeneous Functional of X by LMN7;

        hence x in ( BoundedLinearFunctionals X) by DUALSP01:def 10;

      end;

      ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) = NORMSTR (# ( BoundedLinearOperators (X, RNS_Real )), ( Zero_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( Add_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( Mult_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( BoundedLinearOperatorsNorm (X, RNS_Real )) #) by LOPBAN_1:def 14;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: DUALSP02:15

    for X be RealNormSpace, x,y be Point of ( DualSp X), v,w be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) st x = v & y = w holds (x + y) = (v + w)

    proof

      let X be RealNormSpace, x,y be Point of ( DualSp X), v,w be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

      assume

       AS: x = v & y = w;

      reconsider z = (x + y) as Point of ( DualSp X);

      reconsider u = (v + w) as Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

      

       BX: ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) = NORMSTR (# ( BoundedLinearOperators (X, RNS_Real )), ( Zero_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( Add_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( Mult_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( BoundedLinearOperatorsNorm (X, RNS_Real )) #) by LOPBAN_1:def 14;

      

       A1: z is Lipschitzian additive homogeneous Function of the carrier of X, REAL by DUALSP01:def 10;

      then

       A5: ( dom z) = the carrier of X by FUNCT_2:def 1;

      

       A2: u is Lipschitzian additive homogeneous Function of X, RNS_Real by LOPBAN_1:def 9, BX;

      for t be object st t in ( dom z) holds (z . t) = (u . t)

      proof

        let t be object;

        assume t in ( dom z);

        then

        reconsider t as VECTOR of X by FUNCT_2:def 1, A1;

        (z . t) = ((x . t) + (y . t)) by DUALSP01: 29

        .= ((v . t) + (w . t)) by AS, BINOP_2:def 9;

        hence thesis by LOPBAN_1: 35;

      end;

      hence thesis by A2, A5, FUNCT_2:def 1;

    end;

    theorem :: DUALSP02:16

    

     LMN9: for X be RealNormSpace, a be Element of REAL , x be Point of ( DualSp X), v be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) st x = v holds (a * x) = (a * v)

    proof

      let X be RealNormSpace, a be Element of REAL , x be Point of ( DualSp X), v be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

      assume

       AS: x = v;

      reconsider z = (a * x) as Point of ( DualSp X);

      reconsider u = (a * v) as Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

      

       BX: ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) = NORMSTR (# ( BoundedLinearOperators (X, RNS_Real )), ( Zero_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( Add_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( Mult_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( BoundedLinearOperatorsNorm (X, RNS_Real )) #) by LOPBAN_1:def 14;

      

       A1: z is Lipschitzian additive homogeneous Function of the carrier of X, REAL by DUALSP01:def 10;

      then

       A5: ( dom z) = the carrier of X by FUNCT_2:def 1;

      

       A2: u is Lipschitzian additive homogeneous Function of X, RNS_Real by LOPBAN_1:def 9, BX;

      for t be object st t in ( dom z) holds (z . t) = (u . t)

      proof

        let t be object;

        assume t in ( dom z);

        then

        reconsider t as VECTOR of X by FUNCT_2:def 1, A1;

        (z . t) = (a * (x . t)) by DUALSP01: 30

        .= (a * (v . t)) by AS, BINOP_2:def 11;

        hence thesis by LOPBAN_1: 36;

      end;

      hence thesis by A5, FUNCT_2:def 1, A2;

    end;

    theorem :: DUALSP02:17

    for X be RealNormSpace, x be Point of ( DualSp X), v be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) st x = v holds ( - x) = ( - v)

    proof

      let X be RealNormSpace, x be Point of ( DualSp X), v be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

      assume

       AS: x = v;

      

       A1: ( - 1) is Element of REAL by XREAL_0:def 1;

      

      thus ( - x) = (( - 1) * x) by RLVECT_1: 16

      .= (( - 1) * v) by AS, A1, LMN9

      .= ( - v) by RLVECT_1: 16;

    end;

    theorem :: DUALSP02:18

    

     LMN11: for X be RealNormSpace, x be Point of ( DualSp X), v be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) st x = v holds ||.x.|| = ||.v.||

    proof

      let X be RealNormSpace, x be Point of ( DualSp X), v be Point of ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real ));

      assume

       AS: x = v;

      

       BX: ( R_NormSpace_of_BoundedLinearOperators (X, RNS_Real )) = NORMSTR (# ( BoundedLinearOperators (X, RNS_Real )), ( Zero_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( Add_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( Mult_ (( BoundedLinearOperators (X, RNS_Real )),( R_VectorSpace_of_LinearOperators (X, RNS_Real )))), ( BoundedLinearOperatorsNorm (X, RNS_Real )) #) by LOPBAN_1:def 14;

      reconsider x1 = x as Lipschitzian linear-Functional of X by DUALSP01:def 10;

      reconsider v1 = v as Lipschitzian LinearOperator of X, RNS_Real by LOPBAN_1:def 9, BX;

      now

        let r be Real;

        assume

         AS2: r in ( PreNorms v1);

        ( PreNorms v1) = { ||.(v . t).|| where t be VECTOR of X : ||.t.|| <= 1 } by LOPBAN_1:def 12;

        then

        consider t be VECTOR of X such that

         B1: r = ||.(v . t).|| & ||.t.|| <= 1 by AS2;

         |.(x1 . t).| <= ( ||.x.|| * ||.t.||) by DUALSP01: 26;

        then

         B2: ||.(v . t).|| <= ( ||.x.|| * ||.t.||) by AS, EUCLID:def 2;

        ( ||.x.|| * ||.t.||) <= ( ||.x.|| * 1) by B1, XREAL_1: 64;

        hence r <= ||.x.|| by B1, B2, XXREAL_0: 2;

      end;

      then ( upper_bound ( PreNorms v1)) <= ||.x.|| by SEQ_4: 45;

      then

       A4: ||.v.|| <= ||.x.|| by BX, LOPBAN_1: 30;

      now

        let r be Real;

        assume r in ( PreNorms x1);

        then

        consider t be VECTOR of X such that

         B1: r = |.(x . t).| & ||.t.|| <= 1;

         ||.(v1 . t).|| <= ( ||.v.|| * ||.t.||) by LOPBAN_1: 32;

        then

         B2: |.(x . t).| <= ( ||.v.|| * ||.t.||) by AS, EUCLID:def 2;

        ( ||.v.|| * ||.t.||) <= ( ||.v.|| * 1) by B1, XREAL_1: 64;

        hence r <= ||.v.|| by B1, B2, XXREAL_0: 2;

      end;

      then ( upper_bound ( PreNorms x1)) <= ||.v.|| by SEQ_4: 45;

      then ||.x.|| <= ||.v.|| by DUALSP01: 24;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: DUALSP02:19

    

     Th75: for X be RealNormSpace, L be Subset of X st X is non trivial & (for f be Point of ( DualSp X) holds ex Kf be Real st 0 <= Kf & for x be Point of X st x in L holds |.(f . x).| <= Kf) holds ex M be Real st 0 <= M & for x be Point of X st x in L holds ||.x.|| <= M

    proof

      let X be RealNormSpace, L be Subset of X;

      assume

       AS: X is non trivial & for f be Point of ( DualSp X) holds ex Kf be Real st 0 <= Kf & for x be Point of X st x in L holds |.(f . x).| <= Kf;

      set T = (( BidualFunc X) .: L);

      

       XX: T is Subset of ( R_NormSpace_of_BoundedLinearOperators (( DualSp X), RNS_Real )) by Th75A;

      for f be Point of ( DualSp X) holds ex Kf be Real st 0 <= Kf & for g be Point of ( R_NormSpace_of_BoundedLinearOperators (( DualSp X), RNS_Real )) st g in T holds ||.(g . f).|| <= Kf

      proof

        let f be Point of ( DualSp X);

        consider Kf be Real such that

         A0: 0 <= Kf & for x be Point of X st x in L holds |.(f . x).| <= Kf by AS;

        for g be Point of ( R_NormSpace_of_BoundedLinearOperators (( DualSp X), RNS_Real )) st g in T holds ||.(g . f).|| <= Kf

        proof

          let g be Point of ( R_NormSpace_of_BoundedLinearOperators (( DualSp X), RNS_Real ));

          assume g in T;

          then

          consider x be object such that

           A1: x in ( dom ( BidualFunc X)) & x in L & g = (( BidualFunc X) . x) by FUNCT_1:def 6;

          reconsider x as Point of X by A1;

          

           A2: |.(f . x).| <= Kf by A1, A0;

          g = ( BiDual x) by A1, Def2;

          then (f . x) = (g . f) by Def1;

          hence ||.(g . f).|| <= Kf by A2, EUCLID:def 2;

        end;

        hence thesis by A0;

      end;

      then

      consider M be Real such that

       B0: 0 <= M & for g be Point of ( R_NormSpace_of_BoundedLinearOperators (( DualSp X), RNS_Real )) st g in T holds ||.g.|| <= M by XX, LOPBAN_5: 5;

      

       B1: for x be Point of X st x in L holds ||.x.|| <= M

      proof

        let x be Point of X;

        assume

         B2: x in L;

        x in the carrier of X;

        then

         B3: x in ( dom ( BidualFunc X)) by FUNCT_2:def 1;

        reconsider g = (( BidualFunc X) . x) as Point of ( R_NormSpace_of_BoundedLinearOperators (( DualSp X), RNS_Real )) by Th75A;

        

         B4: g in T by B2, B3, FUNCT_1:def 6;

         ||.x.|| = ||.(( BidualFunc X) . x).|| by AS, LMNORM

        .= ||.g.|| by LMN11;

        hence thesis by B0, B4;

      end;

      take M;

      thus thesis by B1, B0;

    end;

    theorem :: DUALSP02:20

    for X be RealNormSpace, L be non empty Subset of X st X is non trivial & (for f be Point of ( DualSp X) holds ex Y1 be Subset of REAL st Y1 = { |.(f . x).| where x be Point of X : x in L } & ( sup Y1) < +infty ) holds ex Y be Subset of REAL st Y = { ||.x.|| where x be Point of X : x in L } & ( sup Y) < +infty

    proof

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

      assume that

       A1: X is non trivial and

       A2: for f be Point of ( DualSp X) holds ex Y1 be Subset of REAL st Y1 = { |.(f . x).| where x be Point of X : x in L } & ( sup Y1) < +infty ;

      

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

      proof

        let f be Point of ( DualSp X);

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

        consider Y1 be Subset of REAL such that

         B1: Y1 = { |.(f . x).| where x be Point of X : x in L } & ( sup Y1) < +infty by A2;

        reconsider r0 = 0 as Real;

        for r be ExtReal st r in Y1 holds r0 <= r

        proof

          let r be ExtReal;

          assume r in Y1;

          then ex x be Point of X st r = |.(f . x).| & x in L by B1;

          hence r0 <= r by COMPLEX1: 46;

        end;

        then

         U5: r0 is LowerBound of Y1 by XXREAL_2:def 2;

        then

         U3: r0 <= ( inf Y1) by XXREAL_2:def 4;

        consider x0 be object such that

         B11: x0 in L by XBOOLE_0:def 1;

        reconsider x0 as Point of X by B11;

        set y1 = |.(f . x0).|;

        y1 in Y1 by B1, B11;

        then

         U6: ( inf Y1) <= y1 & y1 <= ( sup Y1) by XXREAL_2: 3, XXREAL_2: 4;

        then

         B2: ( sup Y1) in REAL by B1, U3, XXREAL_0: 14;

        reconsider Kf = ( sup Y1) as Real by B2;

        

         BX: for x be Point of X st x in L holds |.(f . x).| <= Kf

        proof

          let x be Point of X;

          assume

           C0: x in L;

          reconsider r = |.(f . x).| as Real;

          r in Y1 by C0, B1;

          hence |.(f . x).| <= Kf by XXREAL_2: 4;

        end;

        take Kf;

        thus thesis by U5, U6, BX, XXREAL_2:def 4;

      end;

      consider M be Real such that

       D1: 0 <= M & for x be Point of X st x in L holds ||.x.|| <= M by A1, A3, Th75;

      set f = ( 0. ( DualSp X));

      consider x0 be object such that

       B11: x0 in L by XBOOLE_0:def 1;

      reconsider x0 as Point of X by B11;

      set y1 = |.(f . x0).|;

      set Y = { ||.x.|| where x be Point of X : x in L };

      

       D2: ||.x0.|| in Y by B11;

      Y c= REAL

      proof

        let z be object;

        assume z in Y;

        then ex x be Point of X st z = ||.x.|| & x in L;

        hence z in REAL ;

      end;

      then

      reconsider Y as non empty Subset of REAL by D2;

      for r be ExtReal st r in Y holds r <= M

      proof

        let r be ExtReal;

        assume r in Y;

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

        hence r <= M by D1;

      end;

      then M is UpperBound of Y by XXREAL_2:def 1;

      then

       D3: ( sup Y) <= M by XXREAL_2:def 3;

      take Y;

      M in REAL by XREAL_0:def 1;

      hence thesis by D3, XXREAL_0: 2, XXREAL_0: 9;

    end;

    begin

    definition

      let X be RealNormSpace;

      :: DUALSP02:def4

      attr X is Reflexive means ( BidualFunc X) is onto;

    end

    theorem :: DUALSP02:21

    

     REFF1: for X be RealNormSpace holds X is Reflexive iff for f be Point of ( DualSp ( DualSp X)) holds ex x be Point of X st for g be Point of ( DualSp X) holds (f . g) = (g . x)

    proof

      let X be RealNormSpace;

      hereby

        assume X is Reflexive;

        then

         A1: ( BidualFunc X) is onto;

        thus for f be Point of ( DualSp ( DualSp X)) holds ex x be Point of X st for g be Point of ( DualSp X) holds (f . g) = (g . x)

        proof

          let f be Point of ( DualSp ( DualSp X));

          consider x be object such that

           A2: x in ( dom ( BidualFunc X)) & f = (( BidualFunc X) . x) by A1, FUNCT_1:def 3;

          reconsider x as Point of X by A2;

          take x;

          f = ( BiDual x) by A2, Def2;

          hence thesis by Def1;

        end;

      end;

      assume

       B1: for f be Point of ( DualSp ( DualSp X)) holds ex x be Point of X st for g be Point of ( DualSp X) holds (f . g) = (g . x);

      for v be object st v in the carrier of ( DualSp ( DualSp X)) holds ex s be object st s in the carrier of X & v = (( BidualFunc X) . s)

      proof

        let v be object;

        assume v in the carrier of ( DualSp ( DualSp X));

        then

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

        consider s be Point of X such that

         B2: for g be Point of ( DualSp X) holds (f . g) = (g . s) by B1;

        take s;

        thus s in the carrier of X;

        f = ( BiDual s) by B2, Def1;

        hence v = (( BidualFunc X) . s) by Def2;

      end;

      then ( BidualFunc X) is onto by FUNCT_2: 10;

      hence thesis;

    end;

    theorem :: DUALSP02:22

    for X be RealNormSpace holds X is Reflexive iff ( Im ( BidualFunc X)) = ( DualSp ( DualSp X))

    proof

      let X be RealNormSpace;

      thus X is Reflexive implies ( Im ( BidualFunc X)) = ( DualSp ( DualSp X)) by NORMSP_3: 46;

      assume

       A1: ( Im ( BidualFunc X)) = ( DualSp ( DualSp X));

      ( dom ( BidualFunc X)) <> {} by FUNCT_2:def 1;

      then ( rng ( BidualFunc X)) <> {} & ( rng ( BidualFunc X)) is linearly-closed by NORMSP_3: 35, RELAT_1: 42;

      then the carrier of ( Lin ( rng ( BidualFunc X))) = ( rng ( BidualFunc X)) by NORMSP_3: 31;

      then ( BidualFunc X) is onto by A1;

      hence X is Reflexive;

    end;

    theorem :: DUALSP02:23

    for X be RealNormSpace st X is non trivial Reflexive holds X is RealBanachSpace

    proof

      let X be RealNormSpace;

      assume

       AS: X is non trivial Reflexive;

      then

       P1: ( BidualFunc X) is onto;

      for seq be sequence of X st seq is Cauchy_sequence_by_Norm holds seq is convergent

      proof

        let seq be sequence of X;

        assume

         P2: seq is Cauchy_sequence_by_Norm;

        reconsider seq1 = (( BidualFunc X) * seq) as sequence of ( DualSp ( DualSp X));

        

         XX: ( BidualFunc X) is additive homogeneous;

        for r be Real st r > 0 holds ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((seq1 . n) - (seq1 . m)).|| < r

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider k be Nat such that

           A1: for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r by P2, RSSPACE3: 8;

          

           AK: for n,m be Nat st n >= k & m >= k holds ||.((seq1 . n) - (seq1 . m)).|| < r

          proof

            let n,m be Nat;

            assume n >= k & m >= k;

            then

             A2: ||.((seq . n) - (seq . m)).|| < r by A1;

            n in NAT & m in NAT by ORDINAL1:def 12;

            then n in ( dom seq) & m in ( dom seq) by FUNCT_2:def 1;

            then

             A4: (seq1 . n) = (( BidualFunc X) . (seq . n)) & (seq1 . m) = (( BidualFunc X) . (seq . m)) by FUNCT_1: 13;

            ((seq . n) - (seq . m)) = ((seq . n) + (( - 1) * (seq . m))) by RLVECT_1: 16;

            then

             A7: (( BidualFunc X) . ((seq . n) - (seq . m))) = ((( BidualFunc X) . (seq . n)) + (( BidualFunc X) . (( - 1) * (seq . m)))) by XX;

            (( BidualFunc X) . (( - 1) * (seq . m))) = (( - 1) * (( BidualFunc X) . (seq . m))) by LOPBAN_1:def 5;

            then (( BidualFunc X) . ((seq . n) - (seq . m))) = ((( BidualFunc X) . (seq . n)) - (( BidualFunc X) . (seq . m))) by A7, RLVECT_1: 16;

            hence thesis by A2, AS, A4, LMNORM;

          end;

          take k;

          thus thesis by AK;

        end;

        then

         P5: seq1 is convergent by LOPBAN_1:def 15, RSSPACE3: 8;

        consider s be Point of X such that

         P7: ( lim seq1) = (( BidualFunc X) . s) by P1, FUNCT_2: 113;

        for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((seq . n) - s).|| < 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 ||.((seq1 . n) - ( lim seq1)).|| < r by P5, NORMSP_1:def 7;

          

           BK: for n be Nat st m <= n holds ||.((seq . n) - s).|| < r

          proof

            let n be Nat;

            assume m <= n;

            then

             B2: ||.((seq1 . n) - ( lim seq1)).|| < r by B1;

            n in NAT by ORDINAL1:def 12;

            then n in ( dom seq) by FUNCT_2:def 1;

            then

             B4: (seq1 . n) = (( BidualFunc X) . (seq . n)) by FUNCT_1: 13;

            ((seq . n) - s) = ((seq . n) + (( - 1) * s)) by RLVECT_1: 16;

            then

             B6: (( BidualFunc X) . ((seq . n) - s)) = ((( BidualFunc X) . (seq . n)) + (( BidualFunc X) . (( - 1) * s))) by XX;

            (( BidualFunc X) . (( - 1) * s)) = (( - 1) * (( BidualFunc X) . s)) by LOPBAN_1:def 5;

            then (( BidualFunc X) . ((seq . n) - s)) = ((( BidualFunc X) . (seq . n)) - (( BidualFunc X) . s)) by B6, RLVECT_1: 16;

            hence thesis by B2, AS, P7, B4, LMNORM;

          end;

          take m;

          thus thesis by BK;

        end;

        hence seq is convergent;

      end;

      hence thesis by LOPBAN_1:def 15;

    end;

    theorem :: DUALSP02:24

    

     Th76: for X be RealBanachSpace, M be non empty Subset of X st X is Reflexive & M is linearly-closed closed holds ( NLin M) is Reflexive

    proof

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

      assume that

       A2: X is Reflexive and

       A3: M is linearly-closed and

       A4: M is closed;

      set M0 = ( NLin M);

      

       X1: the carrier of M0 = M by NORMSP_3: 31, A3;

      

       X2: the carrier of M0 c= the carrier of X by DUALSP01:def 16;

      for y be Point of ( DualSp ( DualSp M0)) holds ex x be Point of M0 st for g be Point of ( DualSp M0) holds (y . g) = (g . x)

      proof

        let y be Point of ( DualSp ( DualSp M0));

        reconsider y1 = y as Lipschitzian linear-Functional of ( DualSp M0) by DUALSP01:def 10;

        defpred P[ Function, Function] means $2 = ($1 | M);

        

         P0: for x be Element of ( DualSp X) holds ex y be Element of ( DualSp M0) st P[x, y]

        proof

          let x be Element of ( DualSp X);

          reconsider x0 = x as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          reconsider y0 = (x0 | M) as Function of M0, REAL by X1, FUNCT_2: 32;

          

           B1: y0 is additive

          proof

            let s,t be Point of M0;

            reconsider s1 = s, t1 = t as Point of X by X2;

            

             C1: (s + t) = (s1 + t1) by NORMSP_3: 28;

            

            thus (y0 . (s + t)) = (x0 . (s + t)) by X1, FUNCT_1: 49

            .= ((x0 . s1) + (x0 . t1)) by C1, HAHNBAN:def 2

            .= (((x0 | M) . s) + (x0 . t)) by X1, FUNCT_1: 49

            .= ((y0 . s) + (y0 . t)) by X1, FUNCT_1: 49;

          end;

          

           B2: y0 is homogeneous

          proof

            let s be Point of M0, r be Real;

            reconsider s1 = s as Point of X by X2;

            

             C2: (r * s) = (r * s1) by NORMSP_3: 28;

            

            thus (y0 . (r * s)) = (x0 . (r * s)) by X1, FUNCT_1: 49

            .= (r * (x0 . s)) by C2, HAHNBAN:def 3

            .= (r * (y0 . s)) by X1, FUNCT_1: 49;

          end;

          for s be Point of M0 holds |.(y0 . s).| <= ( ||.x.|| * ||.s.||)

          proof

            let s be Point of M0;

            reconsider s1 = s as Point of X by X2;

            

             C3: ||.s.|| = ||.s1.|| by NORMSP_3: 28;

             |.(y0 . s).| = |.(x0 . s).| by X1, FUNCT_1: 49;

            hence thesis by C3, DUALSP01: 26;

          end;

          then y0 is Lipschitzian;

          then

          reconsider y = y0 as Element of ( DualSp M0) by B1, B2, DUALSP01:def 10;

          take y;

          thus y = (x | M);

        end;

        consider T be Function of ( DualSp X), ( DualSp M0) such that

         P11: for x be Element of ( DualSp X) holds P[x, (T . x)] from FUNCT_2:sch 3( P0);

        

         D1: T is additive

        proof

          let f,g be Point of ( DualSp X);

          

           E1: (T . (f + g)) is Function of M0, REAL & ((T . f) + (T . g)) is Function of M0, REAL by DUALSP01:def 10;

          for x be Point of M0 holds ((T . (f + g)) . x) = (((T . f) + (T . g)) . x)

          proof

            let x be Point of M0;

            reconsider x1 = x as Point of X by X2;

            (T . f) = (f | M) & (T . g) = (g | M) by P11;

            then

            reconsider fm = (f | M), gm = (g | M) as Point of ( DualSp M0);

            

             F2: (fm . x) = (f . x) & (gm . x) = (g . x) by X1, FUNCT_1: 49;

            

            thus ((T . (f + g)) . x) = (((f + g) | M) . x) by P11

            .= ((f + g) . x) by X1, FUNCT_1: 49

            .= ((f . x1) + (g . x1)) by DUALSP01: 29

            .= (((T . f) . x) + (gm . x)) by P11, F2

            .= (((T . f) . x) + ((T . g) . x)) by P11

            .= (((T . f) + (T . g)) . x) by DUALSP01: 29;

          end;

          hence (T . (f + g)) = ((T . f) + (T . g)) by E1, FUNCT_2:def 8;

        end;

        T is homogeneous

        proof

          let f be Point of ( DualSp X), r be Real;

          

           E3: (T . (r * f)) is Function of M0, REAL & (r * (T . f)) is Function of M0, REAL by DUALSP01:def 10;

          for x be Point of M0 holds ((T . (r * f)) . x) = ((r * (T . f)) . x)

          proof

            let x be Point of M0;

            reconsider x1 = x as Point of X by X2;

            (T . f) = (f | M) by P11;

            then

            reconsider fm = (f | M) as Point of ( DualSp M0);

            

             F4: (fm . x) = (f . x) by X1, FUNCT_1: 49;

            

            thus ((T . (r * f)) . x) = (((r * f) | M) . x) by P11

            .= ((r * f) . x) by X1, FUNCT_1: 49

            .= (r * (f . x1)) by DUALSP01: 30

            .= (r * ((T . f) . x)) by P11, F4

            .= ((r * (T . f)) . x) by DUALSP01: 30;

          end;

          hence (T . (r * f)) = (r * (T . f)) by E3, FUNCT_2:def 8;

        end;

        then

        reconsider T as LinearOperator of ( DualSp X), ( DualSp M0) by D1;

        for v be Point of ( DualSp X) holds ||.(T . v).|| <= (1 * ||.v.||)

        proof

          let v be Point of ( DualSp X);

          reconsider v1 = v as Lipschitzian linear-Functional of X by DUALSP01:def 10;

          

           B0: (T . v) = (v | M) by P11;

          then

          reconsider vm = (v | M) as Point of ( DualSp M0);

          reconsider vm1 = vm as Lipschitzian linear-Functional of M0 by DUALSP01:def 10;

          now

            let r be Real;

            assume r in ( PreNorms vm1);

            then

            consider t be VECTOR of M0 such that

             B1: r = |.(vm1 . t).| & ||.t.|| <= 1;

            reconsider t1 = t as Point of X by X2;

            

             B2: |.(vm . t).| = |.(v . t1).| by X1, FUNCT_1: 49;

             ||.t1.|| = ||.t.|| by NORMSP_3: 28;

            hence r in ( PreNorms v1) by B1, B2;

          end;

          then ( PreNorms vm1) c= ( PreNorms v1);

          then ( upper_bound ( PreNorms vm1)) <= ( upper_bound ( PreNorms v1)) by SEQ_4: 48;

          then ||.vm.|| <= ( upper_bound ( PreNorms v1)) by DUALSP01: 24;

          hence ||.(T . v).|| <= (1 * ||.v.||) by B0, DUALSP01: 24;

        end;

        then

        reconsider T as Lipschitzian LinearOperator of ( DualSp X), ( DualSp M0) by LOPBAN_1:def 8;

        

         P2: for f be Point of ( DualSp X), x be Point of X st x in M holds ((T . f) . x) = (f . x)

        proof

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

          assume x in M;

          then ((f | M) . x) = (f . x) by FUNCT_1: 49;

          hence thesis by P11;

        end;

        deffunc F( Element of ( DualSp X)) = (y . (T . $1));

        consider z be Function of the carrier of ( DualSp X), REAL such that

         Q10: for f be Element of the carrier of ( DualSp X) holds (z . f) = F(f) from FUNCT_2:sch 4;

        

         Q11: z is additive

        proof

          let s,t be Point of ( DualSp X);

          

          thus (z . (s + t)) = (y . (T . (s + t))) by Q10

          .= (y . ((T . s) + (T . t))) by VECTSP_1:def 20

          .= ((y1 . (T . s)) + (y1 . (T . t))) by HAHNBAN:def 2

          .= ((z . s) + (y . (T . t))) by Q10

          .= ((z . s) + (z . t)) by Q10;

        end;

        

         Q12: z is homogeneous

        proof

          let s be Point of ( DualSp X), r be Real;

          

          thus (z . (r * s)) = (y . (T . (r * s))) by Q10

          .= (y . (r * (T . s))) by LOPBAN_1:def 5

          .= (r * (y1 . (T . s))) by HAHNBAN:def 3

          .= (r * (z . s)) by Q10;

        end;

        ( R_NormSpace_of_BoundedLinearOperators (( DualSp X),( DualSp M0))) = NORMSTR (# ( BoundedLinearOperators (( DualSp X),( DualSp M0))), ( Zero_ (( BoundedLinearOperators (( DualSp X),( DualSp M0))),( R_VectorSpace_of_LinearOperators (( DualSp X),( DualSp M0))))), ( Add_ (( BoundedLinearOperators (( DualSp X),( DualSp M0))),( R_VectorSpace_of_LinearOperators (( DualSp X),( DualSp M0))))), ( Mult_ (( BoundedLinearOperators (( DualSp X),( DualSp M0))),( R_VectorSpace_of_LinearOperators (( DualSp X),( DualSp M0))))), ( BoundedLinearOperatorsNorm (( DualSp X),( DualSp M0))) #) by LOPBAN_1:def 14;

        then

        reconsider T1 = T as Point of ( R_NormSpace_of_BoundedLinearOperators (( DualSp X),( DualSp M0))) by LOPBAN_1:def 9;

        for s be Point of ( DualSp X) holds |.(z . s).| <= (( ||.y.|| * ||.T1.||) * ||.s.||)

        proof

          let s be Point of ( DualSp X);

          

           B1: |.(z . s).| = |.(y . (T . s)).| by Q10;

          

           B2: |.(y1 . (T . s)).| <= ( ||.y.|| * ||.(T . s).||) by DUALSP01: 26;

          ( ||.y.|| * ||.(T . s).||) <= ( ||.y.|| * ( ||.T1.|| * ||.s.||)) by XREAL_1: 64, LOPBAN_1: 32;

          hence thesis by B1, B2, XXREAL_0: 2;

        end;

        then z is Lipschitzian;

        then

        reconsider z as Point of ( DualSp ( DualSp X)) by Q11, Q12, DUALSP01:def 10;

        consider x be Point of X such that

         Q2: for f be Point of ( DualSp X) holds (z . f) = (f . x) by A2, REFF1;

        

         Q3: for f be Point of ( DualSp X) holds (y . (T . f)) = (f . x)

        proof

          let f be Point of ( DualSp X);

          

          thus (y . (T . f)) = (z . f) by Q10

          .= (f . x) by Q2;

        end;

        

         AX: x in the carrier of M0

        proof

          assume not x in the carrier of M0;

          then

          consider f be Point of ( DualSp X) such that

           B1: (for x be Point of X st x in M holds (( Bound2Lipschitz (f,X)) . x) = 0 ) and

           B2: (( Bound2Lipschitz (f,X)) . x) = 1 by A3, A4, X1, Lm64;

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

          

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

          

           B4: for x be Point of X st x in M holds ((T . f) . x) = 0

          proof

            let x be Point of X;

            assume

             C1: x in M;

            then (f . x) = 0 by B1, B3;

            hence thesis by C1, P2;

          end;

          

           B8: (T . f) is Function of M0, REAL by DUALSP01:def 10;

          for x be Point of M0 holds ((T . f) . x) = ((M --> 0 ) . x)

          proof

            let x be Point of M0;

            x in M by X1;

            then

            reconsider x1 = x as Point of X;

            ((T . f) . x1) = 0 by X1, B4;

            hence thesis by X1, FUNCOP_1: 7;

          end;

          

          then

           B9: (T . f) = (M --> 0 ) by X1, B8, FUNCT_2:def 8

          .= ( 0. ( DualSp M0)) by X1, DUALSP01: 25;

          (f . x) = (y1 . ( 0. ( DualSp M0))) by B9, Q3

          .= 0 by HAHNBAN: 20;

          hence contradiction by B2, B3;

        end;

        

         Q4: for f be Point of ( DualSp X) holds (y . (T . f)) = ((T . f) . x)

        proof

          let f be Point of ( DualSp X);

          (y . (T . f)) = (f . x) by Q3;

          hence thesis by P2, X1, AX;

        end;

        

         Q5: for f be Point of ( DualSp X) holds (y . (f | M)) = ((f | M) . x)

        proof

          let f be Point of ( DualSp X);

          (T . f) = (f | M) by P11;

          hence thesis by Q4;

        end;

        for g be Point of ( DualSp M0) holds (y . g) = (g . x)

        proof

          let g be Point of ( DualSp M0);

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

          ex f1 be Lipschitzian linear-Functional of X, f be Point of ( DualSp X) st f1 = f & (f1 | the carrier of M0) = g1 & ||.f.|| = ||.g.|| by DUALSP01: 36;

          hence thesis by X1, Q5;

        end;

        hence thesis by AX;

      end;

      hence thesis by REFF1;

    end;

    theorem :: DUALSP02:25

    

     NISOM08: for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, y be Lipschitzian linear-Functional of Y holds (y * L) is Lipschitzian linear-Functional of X

    proof

      let X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, y be Lipschitzian linear-Functional of Y;

      consider M be Real such that

       AS1: 0 <= M & for x be VECTOR of X holds ||.(L . x).|| <= (M * ||.x.||) by LOPBAN_1:def 8;

      

       D1: ( dom L) = the carrier of X by FUNCT_2:def 1;

      set x = (y * L);

      

       P6: for v,w be VECTOR of X holds (x . (v + w)) = ((x . v) + (x . w))

      proof

        let v,w be VECTOR of X;

        

        thus (x . (v + w)) = (y . (L . (v + w))) by D1, FUNCT_1: 13

        .= (y . ((L . v) + (L . w))) by VECTSP_1:def 20

        .= ((y . (L . v)) + (y . (L . w))) by HAHNBAN:def 2

        .= ((x . v) + (y . (L . w))) by D1, FUNCT_1: 13

        .= ((x . v) + (x . w)) by D1, FUNCT_1: 13;

      end;

      for v be VECTOR of X, r be Real holds (x . (r * v)) = (r * (x . v))

      proof

        let v be VECTOR of X, r be Real;

        

        thus (x . (r * v)) = (y . (L . (r * v))) by D1, FUNCT_1: 13

        .= (y . (r * (L . v))) by LOPBAN_1:def 5

        .= (r * (y . (L . v))) by HAHNBAN:def 3

        .= (r * (x . v)) by D1, FUNCT_1: 13;

      end;

      then

      reconsider x as linear-Functional of X by P6, HAHNBAN:def 2, HAHNBAN:def 3;

      consider N be Real such that

       P7: 0 <= N & for v be VECTOR of Y holds |.(y . v).| <= (N * ||.v.||) by DUALSP01:def 9;

      for v be VECTOR of X holds |.(x . v).| <= ((M * N) * ||.v.||)

      proof

        let v be VECTOR of X;

        

         P8: |.(x . v).| = |.(y . (L . v)).| by D1, FUNCT_1: 13;

        

         P9: |.(y . (L . v)).| <= (N * ||.(L . v).||) by P7;

        (N * ||.(L . v).||) <= (N * (M * ||.v.||)) by AS1, P7, XREAL_1: 64;

        hence thesis by P8, P9, XXREAL_0: 2;

      end;

      hence thesis by DUALSP01:def 9, AS1, P7;

    end;

    theorem :: DUALSP02:26

    

     NISOM09: for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y st L is isomorphism holds ex T be Lipschitzian LinearOperator of ( DualSp X), ( DualSp Y) st T is isomorphism & for x be Point of ( DualSp X) holds (T . x) = (x * (L " ))

    proof

      let X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y;

      assume

       AS: L is isomorphism;

      then

       AS1: L is one-to-one & L is onto & for x be Point of X holds ||.x.|| = ||.(L . x).||;

      consider K be Lipschitzian LinearOperator of Y, X such that

       AS2: K = (L " ) & K is isomorphism by AS, NORMSP_3: 37;

      

       D1: ( dom K) = the carrier of Y by FUNCT_2:def 1;

      defpred P[ Function, Function] means $2 = ($1 * K);

      

       P0: for x be Element of ( DualSp X) holds ex y be Element of ( DualSp Y) st P[x, y]

      proof

        let x be Element of ( DualSp X);

        x is Lipschitzian linear-Functional of X by DUALSP01:def 10;

        then (x * K) is Lipschitzian linear-Functional of Y by NISOM08;

        then

        reconsider y = (x * K) as Element of ( DualSp Y) by DUALSP01:def 10;

        take y;

        thus y = (x * K);

      end;

      consider T be Function of ( DualSp X), ( DualSp Y) such that

       P1: for x be Element of ( DualSp X) holds P[x, (T . x)] from FUNCT_2:sch 3( P0);

      for v,w be Point of ( DualSp X) holds (T . (v + w)) = ((T . v) + (T . w))

      proof

        let v,w be Point of ( DualSp X);

        

         P21: (T . v) = (v * K) & (T . w) = (w * K) & (T . (v + w)) = ((v + w) * K) by P1;

        for t be VECTOR of Y holds ((T . (v + w)) . t) = (((T . v) . t) + ((T . w) . t))

        proof

          let t be VECTOR of Y;

          

          thus ((T . (v + w)) . t) = ((v + w) . (K . t)) by P21, D1, FUNCT_1: 13

          .= ((v . (K . t)) + (w . (K . t))) by DUALSP01: 29

          .= (((T . v) . t) + (w . (K . t))) by P21, D1, FUNCT_1: 13

          .= (((T . v) . t) + ((T . w) . t)) by P21, D1, FUNCT_1: 13;

        end;

        hence thesis by DUALSP01: 29;

      end;

      then

       P3: T is additive;

      for v be Point of ( DualSp X), r be Real holds (T . (r * v)) = (r * (T . v))

      proof

        let v be Point of ( DualSp X), r be Real;

        

         P21: (T . v) = (v * K) & (T . (r * v)) = ((r * v) * K) by P1;

        for t be VECTOR of Y holds ((T . (r * v)) . t) = (r * ((T . v) . t))

        proof

          let t be VECTOR of Y;

          

          thus ((T . (r * v)) . t) = ((r * v) . (K . t)) by P21, D1, FUNCT_1: 13

          .= (r * (v . (K . t))) by DUALSP01: 30

          .= (r * ((T . v) . t)) by P21, D1, FUNCT_1: 13;

        end;

        hence thesis by DUALSP01: 30;

      end;

      then

      reconsider T as LinearOperator of ( DualSp X), ( DualSp Y) by P3, LOPBAN_1:def 5;

      for v be object st v in the carrier of ( DualSp Y) holds ex s be object st s in the carrier of ( DualSp X) & v = (T . s)

      proof

        let v be object;

        assume v in the carrier of ( DualSp Y);

        then

        reconsider y = v as Lipschitzian linear-Functional of Y by DUALSP01:def 10;

        (y * L) is Lipschitzian linear-Functional of X by NISOM08;

        then

        reconsider s = (y * L) as Point of ( DualSp X) by DUALSP01:def 10;

        take s;

        

         G6: ( dom y) = the carrier of Y by FUNCT_2:def 1;

        (T . s) = (s * K) by P1

        .= (y * (L * K)) by RELAT_1: 36

        .= (y * ( id ( rng L))) by AS2, AS, FUNCT_1: 39

        .= v by G6, AS1, RELAT_1: 51;

        hence thesis;

      end;

      then

       XX: T is onto by FUNCT_2: 10;

      

       P5: for v be Point of ( DualSp X) holds ||.(T . v).|| = ||.v.||

      proof

        let v be Point of ( DualSp X);

        

         P21: (T . v) = (v * K) by P1;

        reconsider y = (T . v) as Lipschitzian linear-Functional of Y by DUALSP01:def 10;

        reconsider x = v as Lipschitzian linear-Functional of X by DUALSP01:def 10;

        for z be object holds z in ( PreNorms x) iff z in ( PreNorms y)

        proof

          let z be object;

          hereby

            assume z in ( PreNorms x);

            then

            consider t be VECTOR of X such that

             B2: z = |.(x . t).| & ||.t.|| <= 1;

            

             D1: ( dom L) = the carrier of X by FUNCT_2:def 1;

            

             D2: ( dom K) = the carrier of Y by FUNCT_2:def 1;

            set s = (L . t);

            (K . s) = t by AS, AS2, D1, FUNCT_1: 34;

            then

             A81: z = |.(y . s).| by P21, D2, B2, FUNCT_1: 13;

             ||.s.|| = ||.t.|| by AS;

            hence z in ( PreNorms y) by A81, B2;

          end;

          assume z in ( PreNorms y);

          then

          consider s be VECTOR of Y such that

           B2: z = |.(y . s).| & ||.s.|| <= 1;

          set t = (K . s);

          ( dom K) = the carrier of Y by FUNCT_2:def 1;

          then

           A81: z = |.(x . t).| by B2, P21, FUNCT_1: 13;

           ||.s.|| = ||.t.|| by AS2;

          hence z in ( PreNorms x) by A81, B2;

        end;

        then

         A9: ( PreNorms x) = ( PreNorms y);

        

        thus ||.v.|| = ( upper_bound ( PreNorms ( Bound2Lipschitz (v,X)))) by DUALSP01:def 14

        .= ( upper_bound ( PreNorms y)) by A9, DUALSP01: 23

        .= ( upper_bound ( PreNorms ( Bound2Lipschitz (y,Y)))) by DUALSP01: 23

        .= ||.(T . v).|| by DUALSP01:def 14;

      end;

      then for v be Point of ( DualSp X) holds ||.(T . v).|| <= (1 * ||.v.||);

      then

      reconsider T as Lipschitzian LinearOperator of ( DualSp X), ( DualSp Y) by LOPBAN_1:def 8;

      take T;

      for x1,x2 be object st x1 in the carrier of ( DualSp X) & x2 in the carrier of ( DualSp X) & (T . x1) = (T . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A1: x1 in the carrier of ( DualSp X) & x2 in the carrier of ( DualSp X) & (T . x1) = (T . x2);

        then

        reconsider v1 = x1, v2 = x2 as Point of ( DualSp X);

        (T . (v1 - v2)) = (T . (v1 + (( - 1) * v2))) by RLVECT_1: 16

        .= ((T . v1) + (T . (( - 1) * v2))) by VECTSP_1:def 20

        .= ((T . v1) + (( - 1) * (T . v2))) by LOPBAN_1:def 5

        .= ((T . v1) + ( - (T . v2))) by RLVECT_1: 16

        .= ( 0. ( DualSp Y)) by RLVECT_1: 5, A1;

        then ||.(T . (v1 - v2)).|| = 0 ;

        then ||.(v1 - v2).|| = 0 by P5;

        hence thesis by NORMSP_1: 6;

      end;

      hence thesis by P5, XX, P1, AS2, FUNCT_2: 19;

    end;

    

     NISOM11: for X,Y be RealNormSpace st ex L be Lipschitzian LinearOperator of X, Y st L is isomorphism holds (X is Reflexive implies Y is Reflexive)

    proof

      let X,Y be RealNormSpace;

      assume ex L be Lipschitzian LinearOperator of X, Y st L is isomorphism;

      then

      consider L be Lipschitzian LinearOperator of X, Y such that

       AS: L is isomorphism;

      

       AS2: L is one-to-one onto & for x be Point of X holds ||.x.|| = ||.(L . x).|| by AS;

      consider T be Lipschitzian LinearOperator of ( DualSp X), ( DualSp Y) such that

       AS1: T is isomorphism & for x be Point of ( DualSp X) holds (T . x) = (x * (L " )) by NISOM09, AS;

      

       DT: ( dom T) = the carrier of ( DualSp X) by FUNCT_2:def 1;

      assume X is Reflexive;

      then

       P1: ( BidualFunc X) is onto;

      for y be object st y in the carrier of ( DualSp ( DualSp Y)) holds ex x be object st x in the carrier of Y & y = (( BidualFunc Y) . x)

      proof

        let y be object;

        assume y in the carrier of ( DualSp ( DualSp Y));

        then

        reconsider v = y as Point of ( DualSp ( DualSp Y));

        reconsider v as Lipschitzian linear-Functional of ( DualSp Y) by DUALSP01:def 10;

        (v * T) is Lipschitzian linear-Functional of ( DualSp X) by NISOM08;

        then

        reconsider s = (v * T) as Point of ( DualSp ( DualSp X)) by DUALSP01:def 10;

        consider t be object such that

         P2: t in the carrier of X & (( BidualFunc X) . t) = s by P1, FUNCT_2: 11;

        reconsider t as Point of X by P2;

        set u = (L . t);

        take u;

        for z be Point of ( DualSp Y) holds (v . z) = (z . u)

        proof

          let z be Point of ( DualSp Y);

          reconsider z0 = z as Lipschitzian linear-Functional of Y by DUALSP01:def 10;

          (z0 * L) is Lipschitzian linear-Functional of X by NISOM08;

          then

          reconsider q = (z0 * L) as Point of ( DualSp X) by DUALSP01:def 10;

          

           R1: ( BiDual t) = s by P2, Def2;

          

           G4: ( dom L) = the carrier of X by FUNCT_2:def 1;

          z is Lipschitzian linear-Functional of Y by DUALSP01:def 10;

          then

           G6: ( dom z) = the carrier of Y by FUNCT_2:def 1;

          

           G7: (s . q) = (v . (T . q)) by DT, FUNCT_1: 13

          .= (v . (q * (L " ))) by AS1

          .= (v . (z0 * (L * (L " )))) by RELAT_1: 36

          .= (v . (z0 * ( id ( rng L)))) by AS, FUNCT_1: 39

          .= (v . z) by G6, AS2, RELAT_1: 51;

          (s . q) = ((z0 * L) . t) by R1, Def1

          .= (z . u) by G4, FUNCT_1: 13;

          hence thesis by G7;

        end;

        then y = ( BiDual u) by Def1;

        hence thesis by Def2;

      end;

      then ( BidualFunc Y) is onto by FUNCT_2: 10;

      hence Y is Reflexive;

    end;

    theorem :: DUALSP02:27

    for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, T be Lipschitzian LinearOperator of ( DualSp X), ( DualSp Y) st L is isomorphism & T is isomorphism & for x be Point of ( DualSp X) holds (T . x) = (x * (L " )) holds ex S be Lipschitzian LinearOperator of ( DualSp Y), ( DualSp X) st S is isomorphism & S = (T " ) & for y be Point of ( DualSp Y) holds (S . y) = (y * L)

    proof

      let X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, T be Lipschitzian LinearOperator of ( DualSp X), ( DualSp Y);

      assume

       AS1: L is isomorphism & T is isomorphism & for x be Point of ( DualSp X) holds (T . x) = (x * (L " ));

      then

       AS2: L is one-to-one onto & for x be Point of X holds ||.x.|| = ||.(L . x).||;

      consider K be Lipschitzian LinearOperator of Y, X such that

       AS3: K = (L " ) & K is isomorphism by AS1, NORMSP_3: 37;

      

       AS4: T is one-to-one & T is onto & for x be Point of ( DualSp X) holds ||.x.|| = ||.(T . x).|| by AS1;

      consider S be Lipschitzian LinearOperator of ( DualSp Y), ( DualSp X) such that

       AS5: S is isomorphism & for y be Point of ( DualSp Y) holds (S . y) = (y * (K " )) by NISOM09, AS3;

      take S;

      

       P2: (K " ) = L by FUNCT_1: 43, AS1, AS3;

      for y,x be object holds y in the carrier of ( DualSp Y) & (S . y) = x iff x in the carrier of ( DualSp X) & (T . x) = y

      proof

        let y,x be object;

        hereby

          assume

           P31: y in the carrier of ( DualSp Y) & (S . y) = x;

          hence x in the carrier of ( DualSp X) by FUNCT_2: 5;

          reconsider yp = y as Point of ( DualSp Y) by P31;

          reconsider xp = x as Point of ( DualSp X) by P31, FUNCT_2: 5;

          yp is linear-Functional of Y by DUALSP01:def 10;

          then

           G6: ( dom yp) = the carrier of Y by FUNCT_2:def 1;

          

          thus (T . x) = (xp * (L " )) by AS1

          .= ((yp * L) * (L " )) by P2, AS5, P31

          .= (yp * (L * (L " ))) by RELAT_1: 36

          .= (yp * ( id ( rng L))) by AS1, FUNCT_1: 39

          .= y by G6, AS2, RELAT_1: 51;

        end;

        assume

         P32: x in the carrier of ( DualSp X) & (T . x) = y;

        hence y in the carrier of ( DualSp Y) by FUNCT_2: 5;

        reconsider yp = y as Point of ( DualSp Y) by P32, FUNCT_2: 5;

        reconsider xp = x as Point of ( DualSp X) by P32;

        

         G5: ( dom L) = the carrier of X by FUNCT_2:def 1;

        xp is linear-Functional of X by DUALSP01:def 10;

        then

         G6: ( dom xp) = the carrier of X by FUNCT_2:def 1;

        

        thus (S . y) = (yp * L) by P2, AS5

        .= ((xp * (L " )) * L) by AS1, P32

        .= (xp * ((L " ) * L)) by RELAT_1: 36

        .= (xp * ( id ( dom L))) by AS1, FUNCT_1: 39

        .= x by G6, G5, RELAT_1: 51;

      end;

      hence thesis by AS5, P2, FUNCT_2: 28, AS4;

    end;

    theorem :: DUALSP02:28

    

     NISOM12: for X,Y be RealNormSpace st ex L be Lipschitzian LinearOperator of X, Y st L is isomorphism holds (X is Reflexive iff Y is Reflexive)

    proof

      let X,Y be RealNormSpace;

      given L be Lipschitzian LinearOperator of X, Y such that

       AS: L is isomorphism;

      ex K be Lipschitzian LinearOperator of Y, X st K = (L " ) & K is isomorphism by AS, NORMSP_3: 37;

      hence thesis by AS, NISOM11;

    end;

    theorem :: DUALSP02:29

    

     Th74A: for X be RealNormSpace st X is non trivial holds ex L be Lipschitzian LinearOperator of X, ( Im ( BidualFunc X)) st L is isomorphism

    proof

      let X be RealNormSpace;

      assume X is non trivial;

      then

      consider DuX be SubRealNormSpace of ( DualSp ( DualSp X)), L be Lipschitzian LinearOperator of X, DuX such that

       A1: L is bijective & DuX = ( Im ( BidualFunc X)) & (for x be Point of X holds (L . x) = ( BiDual x)) & for x be Point of X holds ||.x.|| = ||.(L . x).|| by IMDDX;

      L is isomorphism by A1;

      hence thesis by A1;

    end;

    

     Lm77R: for X be RealBanachSpace st X is non trivial holds X is Reflexive implies ( DualSp X) is Reflexive

    proof

      let X be RealBanachSpace;

      assume

       AS: X is non trivial;

      thus X is Reflexive implies ( DualSp X) is Reflexive

      proof

        assume

         AS1: X is Reflexive;

        for f be Point of ( DualSp ( DualSp ( DualSp X))) holds ex h be Point of ( DualSp X) st for g be Point of ( DualSp ( DualSp X)) holds (f . g) = (g . h)

        proof

          let f be Point of ( DualSp ( DualSp ( DualSp X)));

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

          deffunc F( Element of X) = (f . ( BiDual $1));

          

           P0: ex h be Function of the carrier of X, REAL st for x be Element of X holds (h . x) = F(x) from FUNCT_2:sch 4;

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

           P1: for x be Point of X holds (h . x) = (f . ( BiDual x)) by P0;

          

           P2: h is additive

          proof

            let x,y be Point of X;

            set g0 = ( BidualFunc X);

            

             C2: g0 is additive homogeneous;

            

            thus (h . (x + y)) = (f . ( BiDual (x + y))) by P1

            .= (f . (g0 . (x + y))) by Def2

            .= (f . ((g0 . x) + (g0 . y))) by C2

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

            .= ((f . ( BiDual x)) + (f . (g0 . y))) by Def2

            .= ((f . ( BiDual x)) + (f . ( BiDual y))) by Def2

            .= ((h . x) + (f . ( BiDual y))) by P1

            .= ((h . x) + (h . y)) by P1;

          end;

          

           P3: h is homogeneous

          proof

            let x be Point of X, r be Real;

            set g0 = ( BidualFunc X);

            

            thus (h . (r * x)) = (f . ( BiDual (r * x))) by P1

            .= (f . (g0 . (r * x))) by Def2

            .= (f . (r * (g0 . x))) by LOPBAN_1:def 5

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

            .= (r * (f . ( BiDual x))) by Def2

            .= (r * (h . x)) by P1;

          end;

          for x be Point of X holds |.(h . x).| <= ( ||.f.|| * ||.x.||)

          proof

            let x be Point of X;

            set g0 = ( BidualFunc X);

            

             P5: (h . x) = (f . ( BiDual x)) by P1

            .= (f . (g0 . x)) by Def2;

             |.(f1 . (g0 . x)).| <= ( ||.f.|| * ||.(g0 . x).||) by DUALSP01: 26;

            hence thesis by P5, AS, LMNORM;

          end;

          then h is Lipschitzian;

          then h is Point of ( DualSp X) by P2, P3, DUALSP01:def 10;

          then

          consider h be Point of ( DualSp X) such that

           B1: for x be Point of X holds (h . x) = (f . ( BiDual x)) by P1;

          

           B2: ( BidualFunc X) is onto by AS1;

          set g0 = ( BidualFunc X);

          

           BX: for g be Point of ( DualSp ( DualSp X)) holds (f . g) = (g . h)

          proof

            let g be Point of ( DualSp ( DualSp X));

            consider x be object such that

             C1: x in ( dom g0) & g = (g0 . x) by B2, FUNCT_1:def 3;

            reconsider x as Point of X by C1;

            (f . ( BiDual x)) = (h . x) by B1

            .= (( BiDual x) . h) by Def1;

            

            hence (f . g) = (( BiDual x) . h) by C1, Def2

            .= (g . h) by C1, Def2;

          end;

          take h;

          thus thesis by BX;

        end;

        hence ( DualSp X) is Reflexive by REFF1;

      end;

    end;

    theorem :: DUALSP02:30

    for X be RealBanachSpace st X is non trivial holds X is Reflexive iff ( DualSp X) is Reflexive

    proof

      let X be RealBanachSpace;

      assume

       AS: X is non trivial;

      hence X is Reflexive implies ( DualSp X) is Reflexive by Lm77R;

      assume

       AS2: ( DualSp X) is Reflexive;

      ( DualSp X) is non trivial by AS, Lm65A1;

      then

       C2: ( DualSp ( DualSp X)) is Reflexive by AS2, Lm77R;

      consider L be Lipschitzian LinearOperator of X, ( Im ( BidualFunc X)) such that

       C3: L is isomorphism by AS, Th74A;

      set f = ( BidualFunc X);

      set V = ( DualSp ( DualSp X));

      

       D0: ( rng f) is linearly-closed by NORMSP_3: 35;

      

       D1: ( rng f) <> {}

      proof

        assume ( rng f) = {} ;

        then ( dom f) = {} by RELAT_1: 42;

        hence thesis by FUNCT_2:def 1;

      end;

      then

       C4: the carrier of ( Im f) = ( rng f) by NORMSP_3: 31, D0;

      ( Im f) is complete by C3, NORMSP_3: 44;

      then ( rng f) is closed by C4, NORMSP_3: 48;

      then ( Im f) is Reflexive by C2, D0, Th76, D1;

      hence X is Reflexive by C3, NISOM12;

    end;