dualsp04.miz



    begin

    definition

      let X be RealUnitarySpace;

      :: DUALSP04:def1

      func normRU X -> Function of the carrier of X, REAL means

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

      existence

      proof

        deffunc F( Element of the carrier of X) = ||.$1.||;

        

         X0: for x be Element of the carrier of X holds F(x) in REAL by XREAL_0:def 1;

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

         X1: for x be Element of the carrier of X holds (f . x) = F(x) from FUNCT_2:sch 8( X0);

        take f;

        thus thesis by X1;

      end;

      uniqueness

      proof

        let f1,f2 be Function of the carrier of X, REAL such that

         A1: for x be Point of X holds (f1 . x) = ||.x.|| and

         A2: for x be Point of X holds (f2 . x) = ||.x.||;

        now

          let x be Element of the carrier of X;

          

          thus (f1 . x) = ||.x.|| by A1

          .= (f2 . x) by A2;

        end;

        hence f1 = f2;

      end;

    end

    

     Lm01: for X be RealUnitarySpace holds NORMSTR (# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, ( normRU X) #) is non empty RealNormSpace

    proof

      let X be RealUnitarySpace;

      set T = NORMSTR (# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, ( normRU X) #);

      reconsider T as non empty NORMSTR;

      now

        let v,w be Element of T;

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

        

        thus (v + w) = (v1 + w1)

        .= (w1 + v1)

        .= (w + v);

      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 X;

        

        thus ((u + v) + w) = ((u1 + v1) + w1)

        .= (u1 + (v1 + w1)) by RLVECT_1:def 3

        .= (u + (v + w));

      end;

      then

       A2: T is add-associative;

      now

        let v be Element of T;

        reconsider v1 = v as Element of X;

        

        thus (v + ( 0. T)) = (v1 + ( 0. X))

        .= 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 X;

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

        reconsider w = w1 as Element of T;

        take w;

        

        thus (v + w) = (v1 + w1)

        .= ( 0. X) by RLVECT_1:def 10

        .= ( 0. T);

      end;

      now

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

        reconsider v1 = v as Element of X;

        

        thus ((a + b) * v) = ((a + b) * v1)

        .= ((a * v1) + (b * v1)) by RLVECT_1:def 6

        .= ((a * v) + (b * v));

      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 X;

        

        thus (a * (v + w)) = (a * (v1 + w1))

        .= ((a * v1) + (a * w1)) by RLVECT_1:def 5

        .= ((a * v) + (a * w));

      end;

      then

       A6: T is vector-distributive;

      now

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

        reconsider v1 = v as Element of X;

        

        thus ((a * b) * v) = ((a * b) * v1)

        .= (a * (b * v1)) by RLVECT_1:def 7

        .= (a * (b * v));

      end;

      then

       A7: T is scalar-associative;

      now

        let v be Element of T;

        reconsider v1 = v as Element of X;

        

        thus (1 * v) = (1 * v1)

        .= v by RLVECT_1:def 8;

      end;

      then

       A8: T is scalar-unital;

       ||.( 0. X).|| = 0 by SQUARE_1: 17, BHSP_1: 1;

      then

       A9: T is reflexive by Def1;

      now

        let v be Element of T;

        assume

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

        reconsider v1 = v as Element of X;

         ||.v1.|| = 0 by AS, Def1;

        then v1 = ( 0. X) by BHSP_1: 26;

        hence v = ( 0. T);

      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 X;

        

        thus ||.(a * v).|| = ||.(a * v1).|| by Def1

        .= ( |.a.| * ||.v1.||) by BHSP_1: 27

        .= ( |.a.| * ||.v.||) by Def1;

        

         C3: ||.(v + w).|| = ||.(v1 + w1).|| by Def1;

        ( ||.v.|| + ||.w.||) = ( ||.v1.|| + (( normRU X) . w)) by Def1

        .= ( ||.v1.|| + ||.w1.||) by Def1;

        hence ||.(v + w).|| <= ( ||.v.|| + ||.w.||) by C3, BHSP_1: 30;

      end;

      then T is RealNormSpace-like;

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

    end;

    definition

      let X be RealUnitarySpace;

      :: DUALSP04:def2

      func RUSp2RNSp X -> RealNormSpace equals NORMSTR (# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, ( normRU X) #);

      correctness by Lm01;

    end

    theorem :: DUALSP04:1

    

     RHS3: for X be RealUnitarySpace, x be Point of X, x1 be Point of ( RUSp2RNSp X) st x = x1 holds ( - x) = ( - x1)

    proof

      let X be RealUnitarySpace, x be Point of X, x1 be Point of ( RUSp2RNSp X);

      assume

       AS: x = x1;

      

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

      .= (( - 1) * x1) by AS

      .= ( - x1) by RLVECT_1: 16;

    end;

    theorem :: DUALSP04:2

    

     RHS4: for X be RealUnitarySpace, x,y be Point of X, x1,y1 be Point of ( RUSp2RNSp X) st x = x1 & y = y1 holds (x - y) = (x1 - y1) by RHS3;

    theorem :: DUALSP04:3

    

     RHS6: for X be RealUnitarySpace, x be Point of X, x1 be Point of ( RUSp2RNSp X) st x = x1 holds ||.x.|| = ||.x1.|| by Def1;

    theorem :: DUALSP04:4

    

     RHS8: for X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of ( RUSp2RNSp X) st s1 = s2 holds s1 is convergent iff s2 is convergent

    proof

      let X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of ( RUSp2RNSp X);

      assume

       AS: s1 = s2;

      hereby

        assume

         P1: s1 is convergent;

        reconsider g1 = ( lim s1) as Point of ( RUSp2RNSp X);

        now

          let p be Real;

          assume 0 < p;

          then

          consider m be Nat such that

           P2: for n be Nat st m <= n holds ||.((s1 . n) - ( lim s1)).|| < p by P1, BHSP_2: 19;

          take m;

          thus for n be Nat st m <= n holds ||.((s2 . n) - g1).|| < p

          proof

            let n be Nat;

            assume m <= n;

            then

             P3: ||.((s1 . n) - ( lim s1)).|| < p by P2;

            ((s1 . n) - ( lim s1)) = ((s2 . n) - g1) by AS, RHS3;

            hence ||.((s2 . n) - g1).|| < p by P3, Def1;

          end;

        end;

        hence s2 is convergent;

      end;

      assume

       P4: s2 is convergent;

      reconsider g2 = ( lim s2) as Point of X;

      now

        let p be Real;

        assume 0 < p;

        then

        consider m be Nat such that

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

        take m;

        thus for n be Nat st m <= n holds ||.((s1 . n) - g2).|| < p

        proof

          let n be Nat;

          assume m <= n;

          then

           P3: ||.((s2 . n) - ( lim s2)).|| < p by P2;

          ((s2 . n) - ( lim s2)) = ((s1 . n) - g2) by AS, RHS3;

          hence ||.((s1 . n) - g2).|| < p by P3, Def1;

        end;

      end;

      hence s1 is convergent by BHSP_2: 9;

    end;

    theorem :: DUALSP04:5

    

     RHS9: for X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of ( RUSp2RNSp X) st s1 = s2 & s1 is convergent holds ( lim s1) = ( lim s2)

    proof

      let X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of ( RUSp2RNSp X);

      assume

       AS: s1 = s2;

      assume

       P1: s1 is convergent;

      then

       P5: s2 is convergent by AS, RHS8;

      reconsider g1 = ( lim s1) as Point of ( RUSp2RNSp X);

      now

        let p be Real;

        assume 0 < p;

        then

        consider m be Nat such that

         P2: for n be Nat st m <= n holds ||.((s1 . n) - ( lim s1)).|| < p by P1, BHSP_2: 19;

        take m;

        thus for n be Nat st m <= n holds ||.((s2 . n) - g1).|| < p

        proof

          let n be Nat;

          assume m <= n;

          then

           P3: ||.((s1 . n) - ( lim s1)).|| < p by P2;

          ((s1 . n) - ( lim s1)) = ((s2 . n) - g1) by AS, RHS3;

          hence ||.((s2 . n) - g1).|| < p by P3, Def1;

        end;

      end;

      hence ( lim s2) = ( lim s1) by P5, NORMSP_1:def 7;

    end;

    theorem :: DUALSP04:6

    

     RHS11a: for X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of ( RUSp2RNSp X) st s1 = s2 holds s2 is Cauchy_sequence_by_Norm iff s1 is Cauchy

    proof

      let X be RealUnitarySpace, s1 be sequence of X, s2 be sequence of ( RUSp2RNSp X);

      assume

       A0: s1 = s2;

      hereby

        assume

         AS: s2 is Cauchy_sequence_by_Norm;

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

        proof

          let r be Real;

          assume 0 < r;

          then

          consider k be Nat such that

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

          take k;

          thus for n,m be Nat st n >= k & m >= k holds ||.((s1 . n) - (s1 . m)).|| < r

          proof

            let n,m be Nat;

            assume n >= k & m >= k;

            then

             P2: ||.((s2 . n) - (s2 . m)).|| < r by P1;

            ((s2 . n) - (s2 . m)) = ((s1 . n) - (s1 . m)) by A0, RHS3;

            hence ||.((s1 . n) - (s1 . m)).|| < r by Def1, P2;

          end;

        end;

        hence s1 is Cauchy by BHSP_3: 2;

      end;

      assume

       A1: s1 is Cauchy;

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

      proof

        let r be Real;

        assume r > 0 ;

        then

        consider k be Nat such that

         A2: for n,m be Nat st n >= k & m >= k holds ||.((s1 . n) - (s1 . m)).|| < r by A1, BHSP_3: 2;

        take k;

        thus for n,m be Nat st n >= k & m >= k holds ||.((s2 . n) - (s2 . m)).|| < r

        proof

          let n,m be Nat;

          assume n >= k & m >= k;

          then

           A3: ||.((s1 . n) - (s1 . m)).|| < r by A2;

          ((s1 . n) - (s1 . m)) = ((s2 . n) - (s2 . m)) by A0, RHS3;

          hence ||.((s2 . n) - (s2 . m)).|| < r by Def1, A3;

        end;

      end;

      hence s2 is Cauchy_sequence_by_Norm by RSSPACE3: 8;

    end;

    theorem :: DUALSP04:7

    

     RHS11b: for X be RealUnitarySpace holds X is complete iff ( RUSp2RNSp X) is complete

    proof

      let X be RealUnitarySpace;

      set Y = ( RUSp2RNSp X);

      hereby

        assume

         AS1: X is complete;

        for s2 be sequence of Y holds s2 is Cauchy_sequence_by_Norm implies s2 is convergent

        proof

          let s2 be sequence of Y;

          reconsider s1 = s2 as sequence of X;

          assume s2 is Cauchy_sequence_by_Norm;

          then s1 is Cauchy by RHS11a;

          then s1 is convergent by AS1, BHSP_3:def 4;

          hence s2 is convergent by RHS8;

        end;

        hence Y is complete by LOPBAN_1:def 15;

      end;

      assume

       AS2: Y is complete;

      for s1 be sequence of X holds s1 is Cauchy implies s1 is convergent

      proof

        let s1 be sequence of X;

        reconsider s2 = s1 as sequence of Y;

        assume s1 is Cauchy;

        then s2 is Cauchy_sequence_by_Norm by RHS11a;

        then s2 is convergent by AS2, LOPBAN_1:def 15;

        hence s1 is convergent by RHS8;

      end;

      hence X is complete by BHSP_3:def 4;

    end;

    registration

      let X be RealHilbertSpace;

      cluster ( RUSp2RNSp X) -> complete;

      correctness by RHS11b;

    end

    definition

      let X be RealUnitarySpace, Y be Subset of X;

      :: DUALSP04:def3

      attr Y is open means ex Z be Subset of ( RUSp2RNSp X) st Z = Y & Z is open;

    end

    definition

      let X be RealUnitarySpace, Y be Subset of X;

      :: DUALSP04:def4

      attr Y is closed means ex Z be Subset of ( RUSp2RNSp X) st Z = Y & Z is closed;

    end

    theorem :: DUALSP04:8

    

     LM1: for X be RealUnitarySpace, Y be Subset of X holds Y is closed iff for s be sequence of X st ( rng s) c= Y & s is convergent holds ( lim s) in Y

    proof

      let X be RealUnitarySpace, Y be Subset of X;

      hereby

        assume Y is closed;

        then

        consider Z be Subset of ( RUSp2RNSp X) such that

         A1: Z = Y & Z is closed;

        thus for s be sequence of X st ( rng s) c= Y & s is convergent holds ( lim s) in Y

        proof

          let s be sequence of X;

          assume

           A3: ( rng s) c= Y & s is convergent;

          reconsider s1 = s as sequence of ( RUSp2RNSp X);

          ( rng s1) c= Z & s1 is convergent by A3, A1, RHS8;

          then ( lim s1) in Z by A1;

          hence ( lim s) in Y by A1, A3, RHS9;

        end;

      end;

      assume

       A4: for s be sequence of X st ( rng s) c= Y & s is convergent holds ( lim s) in Y;

      reconsider Z = Y as Subset of ( RUSp2RNSp X);

      for s1 be sequence of ( RUSp2RNSp X) st ( rng s1) c= Z & s1 is convergent holds ( lim s1) in Z

      proof

        let s1 be sequence of ( RUSp2RNSp X);

        assume

         A5: ( rng s1) c= Z & s1 is convergent;

        reconsider s = s1 as sequence of X;

        

         A6: ( rng s) c= Y & s is convergent by A5, RHS8;

        then ( lim s) in Y by A4;

        hence ( lim s1) in Z by A6, RHS9;

      end;

      then Z is closed;

      hence Y is closed;

    end;

    theorem :: DUALSP04:9

    for X be RealUnitarySpace, Y be Subset of X holds Y is open iff (Y ` ) is closed

    proof

      let X be RealUnitarySpace, Y be Subset of X;

      thus Y is open implies (Y ` ) is closed;

      assume (Y ` ) is closed;

      then

      consider Z be Subset of ( RUSp2RNSp X) such that

       A2: Z = (Y ` ) & Z is closed;

      (Z ` ) is open by A2;

      hence Y is open by A2;

    end;

    definition

      let X be RealUnitarySpace;

      let f be PartFunc of the carrier of X, REAL ;

      let x0 be Point of X;

      :: DUALSP04:def5

      pred f is_continuous_in x0 means x0 in ( dom f) & for s1 be sequence of X st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

    end

    definition

      let X be RealUnitarySpace;

      let f be PartFunc of the carrier of X, REAL ;

      let Y be set;

      :: DUALSP04:def6

      pred f is_continuous_on Y means Y c= ( dom f) & for x0 be Point of X st x0 in Y holds (f | Y) is_continuous_in x0;

    end

    theorem :: DUALSP04:10

    

     LM3B: for X be RealUnitarySpace, f be Function of X, REAL , g be Function of ( RUSp2RNSp X), REAL , x0 be Point of X, y0 be Point of ( RUSp2RNSp X) st f = g & x0 = y0 holds f is_continuous_in x0 iff g is_continuous_in y0

    proof

      let X be RealUnitarySpace, f be Function of X, REAL , g be Function of ( RUSp2RNSp X), REAL , x0 be Point of X, y0 be Point of ( RUSp2RNSp X);

      assume

       AS: f = g & x0 = y0;

      set Y = ( RUSp2RNSp X);

      hereby

        assume

         A11: f is_continuous_in x0;

        for s2 be sequence of Y st ( rng s2) c= ( dom g) & s2 is convergent & ( lim s2) = y0 holds (g /* s2) is convergent & (g /. y0) = ( lim (g /* s2))

        proof

          let s2 be sequence of Y;

          assume

           AS1: ( rng s2) c= ( dom g) & s2 is convergent & ( lim s2) = y0;

          reconsider s1 = s2 as sequence of X;

          

           B2: s1 is convergent by AS1, RHS8;

          then ( lim s1) = x0 by AS1, AS, RHS9;

          hence (g /* s2) is convergent & (g /. y0) = ( lim (g /* s2)) by AS, A11, AS1, B2;

        end;

        hence g is_continuous_in y0 by A11, AS;

      end;

      assume

       A31: g is_continuous_in y0;

      for s1 be sequence of X st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1))

      proof

        let s1 be sequence of X;

        assume

         AS2: ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0;

        reconsider s2 = s1 as sequence of Y;

        

         B2: s2 is convergent by AS2, RHS8;

        ( lim s2) = y0 by AS, AS2, RHS9;

        hence (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1)) by AS, A31, AS2, B2;

      end;

      hence f is_continuous_in x0 by A31, AS;

    end;

    theorem :: DUALSP04:11

    

     LM3C: for X be RealUnitarySpace, f be Function of X, REAL , g be Function of ( RUSp2RNSp X), REAL st f = g holds f is_continuous_on the carrier of X iff g is_continuous_on the carrier of ( RUSp2RNSp X)

    proof

      let X be RealUnitarySpace, f be Function of X, REAL , g be Function of ( RUSp2RNSp X), REAL ;

      assume

       AS: f = g;

      set Y = ( RUSp2RNSp X);

      hereby

        assume

         A11: f is_continuous_on the carrier of X;

        for y0 be Point of Y st y0 in the carrier of Y holds (g | the carrier of Y) is_continuous_in y0

        proof

          let y0 be Point of Y;

          assume y0 in the carrier of Y;

          reconsider x0 = y0 as Point of X;

          (f | the carrier of X) is_continuous_in x0 by A11;

          hence thesis by LM3B, AS;

        end;

        hence g is_continuous_on the carrier of Y by A11, AS;

      end;

      assume

       A31: g is_continuous_on the carrier of Y;

      for x0 be Point of X st x0 in the carrier of X holds (f | the carrier of X) is_continuous_in x0

      proof

        let x0 be Point of X;

        assume x0 in the carrier of X;

        reconsider y0 = x0 as Point of Y;

        (g | the carrier of Y) is_continuous_in y0 by A31;

        hence thesis by LM3B, AS;

      end;

      hence thesis by A31, AS;

    end;

    theorem :: DUALSP04:12

    for X be RealUnitarySpace, w be Point of X, f be Function of X, REAL st for v be Point of X holds (f . v) = (w .|. v) holds f is_continuous_on the carrier of X

    proof

      let X be RealUnitarySpace, w be Point of X, f be Function of X, REAL ;

      assume

       AS: for v be Point of X holds (f . v) = (w .|. v);

      set Y = ( RUSp2RNSp X);

      reconsider g = f as Function of Y, REAL ;

      

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

      for y0 be Point of Y st y0 in the carrier of Y holds (g | the carrier of Y) is_continuous_in y0

      proof

        let y0 be Point of Y;

        assume y0 in the carrier of Y;

        for r be Real st 0 < r holds ex s be Real st 0 < s & for y1 be Point of Y st y1 in ( dom g) & ||.(y1 - y0).|| < s holds |.((g /. y1) - (g /. y0)).| < r

        proof

          let r be Real;

          assume

           AS1: 0 < r;

          thus ex s be Real st 0 < s & for y1 be Point of Y st y1 in ( dom g) & ||.(y1 - y0).|| < s holds |.((g /. y1) - (g /. y0)).| < r

          proof

            

             C1: 0 <= ||.w.|| by BHSP_1: 28;

            reconsider s = (r / ( ||.w.|| + 1)) as Real;

            

             C41: ( ||.w.|| + 0 ) < ( ||.w.|| + 1) by XREAL_1: 8;

            (s * ( ||.w.|| + 1)) = r by C1, XCMPLX_1: 87;

            then

             C5: 0 < s & (s * ||.w.||) < r by C1, AS1, C41, XREAL_1: 68;

            

             C6: for y1 be Point of Y st y1 in ( dom g) & ||.(y1 - y0).|| < s holds |.((g /. y1) - (g /. y0)).| < r

            proof

              let y1 be Point of Y;

              assume

               AS2: y1 in ( dom g) & ||.(y1 - y0).|| < s;

              reconsider x1 = y1 as Point of X;

              reconsider x0 = y0 as Point of X;

              

               X0: ||.(y1 - y0).|| = ||.(x1 - x0).|| by RHS4, RHS6;

              

               D1: |.((g /. y1) - (g /. y0)).| = |.((w .|. x1) - (g . y0)).| by AS

              .= |.((w .|. x1) - (w .|. x0)).| by AS

              .= |.(w .|. (x1 - x0)).| by BHSP_1: 12;

              

               D2: |.(w .|. (x1 - x0)).| <= ( ||.w.|| * ||.(x1 - x0).||) by BHSP_1: 29;

              ( ||.w.|| * ||.(x1 - x0).||) <= ( ||.w.|| * s) by X0, C1, AS2, XREAL_1: 64;

              then |.((g /. y1) - (g /. y0)).| <= ( ||.w.|| * s) by D1, D2, XXREAL_0: 2;

              hence |.((g /. y1) - (g /. y0)).| < r by C5, XXREAL_0: 2;

            end;

            take s;

            thus thesis by C1, AS1, C6;

          end;

        end;

        hence (g | the carrier of Y) is_continuous_in y0 by A3, NFCONT_1: 8;

      end;

      then g is_continuous_on the carrier of Y by FUNCT_2:def 1;

      hence thesis by LM3C;

    end;

    definition

      let X be RealUnitarySpace;

      let Y be set;

      let f be PartFunc of the carrier of X, REAL ;

      :: DUALSP04:def7

      pred f is_Lipschitzian_on Y means Y c= ( dom f) & ex r be Real st 0 < r & for x1,x2 be Point of X st x1 in Y & x2 in Y holds |.((f /. x1) - (f /. x2)).| <= (r * ||.(x1 - x2).||);

    end

    theorem :: DUALSP04:13

    

     LM4: for X be RealUnitarySpace, f be Function of X, REAL , g be Function of ( RUSp2RNSp X), REAL st f = g holds f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of ( RUSp2RNSp X)

    proof

      let X be RealUnitarySpace, f be Function of X, REAL , g be Function of ( RUSp2RNSp X), REAL ;

      assume

       AS: f = g;

      set Y = ( RUSp2RNSp X);

      thus f is_Lipschitzian_on the carrier of X implies g is_Lipschitzian_on the carrier of ( RUSp2RNSp X)

      proof

        assume

         A11: f is_Lipschitzian_on the carrier of X;

        then

        consider r be Real such that

         A2: 0 < r & for x1,x2 be Point of X st x1 in the carrier of X & x2 in the carrier of X holds |.((f /. x1) - (f /. x2)).| <= (r * ||.(x1 - x2).||);

        for y1,y2 be Point of Y st y1 in the carrier of Y & y2 in the carrier of Y holds |.((g /. y1) - (g /. y2)).| <= (r * ||.(y1 - y2).||)

        proof

          let y1,y2 be Point of Y;

          assume y1 in the carrier of Y & y2 in the carrier of Y;

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

           ||.(y1 - y2).|| = ||.(x1 - x2).|| by RHS4, RHS6;

          hence |.((g /. y1) - (g /. y2)).| <= (r * ||.(y1 - y2).||) by A2, AS;

        end;

        hence g is_Lipschitzian_on the carrier of Y by A2, A11, AS;

      end;

      assume

       A11: g is_Lipschitzian_on the carrier of Y;

      then

      consider r be Real such that

       A2: 0 < r & for y1,y2 be Point of Y st y1 in the carrier of Y & y2 in the carrier of Y holds |.((g /. y1) - (g /. y2)).| <= (r * ||.(y1 - y2).||);

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

      proof

        let x1,x2 be Point of X;

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

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

         ||.(x1 - x2).|| = ||.(y1 - y2).|| by RHS4, RHS6;

        hence |.((f /. x1) - (f /. x2)).| <= (r * ||.(x1 - x2).||) by A2, AS;

      end;

      hence thesis by A2, A11, AS;

    end;

    theorem :: DUALSP04:14

    

     LM5: for X be RealUnitarySpace, f be Function of X, REAL st f is_Lipschitzian_on the carrier of X holds f is_continuous_on the carrier of X

    proof

      let X be RealUnitarySpace, f be Function of X, REAL ;

      assume

       AS: f is_Lipschitzian_on the carrier of X;

      reconsider g = f as Function of ( RUSp2RNSp X), REAL ;

      set Y = ( RUSp2RNSp X);

      g is_Lipschitzian_on the carrier of Y by AS, LM4;

      then g is_continuous_on the carrier of Y by NFCONT_1: 46;

      hence thesis by LM3C;

    end;

    

     Th16: for X be RealUnitarySpace, f be linear-Functional of X st (for x be VECTOR of X holds (f . x) = 0 ) holds f is Lipschitzian

    proof

      let X be RealUnitarySpace;

      let f be linear-Functional of X;

      assume

       A1: for x be VECTOR of X holds (f . x) = 0 ;

      for x be VECTOR of X holds |.(f . x).| <= (1 * ||.x.||)

      proof

        let x be VECTOR of X;

         0 <= ||.x.|| by BHSP_1: 28;

        hence thesis by A1, COMPLEX1: 44;

      end;

      hence thesis by BHSP_6:def 4;

    end;

    theorem :: DUALSP04:15

    

     Th21X: for X be RealUnitarySpace, F be linear-Functional of X st F = (the carrier of X --> 0 ) holds F is Lipschitzian

    proof

      let X be RealUnitarySpace, F be linear-Functional of X;

      assume F = (the carrier of X --> 0 );

      then for x be VECTOR of X holds (F . x) = 0 ;

      hence thesis by Th16;

    end;

    registration

      let X be RealUnitarySpace;

      cluster Lipschitzian for linear-Functional of X;

      correctness

      proof

        set f = (the carrier of X --> 0 );

        reconsider f as linear-Functional of X by DUALSP01: 9;

        f is Lipschitzian by Th21X;

        hence thesis;

      end;

    end

    definition

      let X be RealUnitarySpace;

      :: DUALSP04:def8

      func BoundedLinearFunctionals X -> Subset of (X *' ) means

      : Def10: for x be set holds x in it iff x is Lipschitzian linear-Functional of X;

      existence

      proof

        defpred P[ object] means $1 is Lipschitzian linear-Functional of X;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( LinearFunctionals X) & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in ( LinearFunctionals X) by A1;

        hence IT is Subset of (X *' ) by TARSKI:def 3;

        let x be set;

        thus x in IT implies x is Lipschitzian linear-Functional of X by A1;

        assume

         A2: x is Lipschitzian linear-Functional of X;

        then x in ( LinearFunctionals X) by DUALSP01:def 6;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of (X *' );

        assume that

         A3: for x be set holds x in X1 iff x is Lipschitzian linear-Functional of X and

         A4: for x be set holds x in X2 iff x is Lipschitzian linear-Functional of X;

        now

          let x be object;

          assume x in X2;

          then x is Lipschitzian linear-Functional of X by A4;

          hence x in X1 by A3;

        end;

        then

         A5: X2 c= X1;

        now

          let x be object;

          assume x in X1;

          then x is Lipschitzian linear-Functional of X by A3;

          hence x in X2 by A4;

        end;

        then X1 c= X2;

        hence thesis by A5;

      end;

    end

    

     Th17: for X be RealUnitarySpace holds ( BoundedLinearFunctionals X) is linearly-closed

    proof

      let X be RealUnitarySpace;

      set W = ( BoundedLinearFunctionals X);

      

       A1: for v,u be VECTOR of (X *' ) st v in W & u in W holds (v + u) in W

      proof

        let v,u be VECTOR of (X *' ) such that

         A2: v in W & u in W;

        reconsider f = (v + u) as linear-Functional of X by DUALSP01:def 6;

        f is Lipschitzian

        proof

          reconsider v1 = v, u1 = u as Lipschitzian linear-Functional of X by A2, Def10;

          consider K2 be Real such that

           A4: 0 < K2 and

           A5: for x be Point of X holds |.(v1 . x).| <= (K2 * ||.x.||) by BHSP_6:def 4;

          consider K1 be Real such that

           A6: 0 < K1 and

           A7: for x be Point of X holds |.(u1 . x).| <= (K1 * ||.x.||) by BHSP_6:def 4;

          reconsider K3 = (K1 + K2) as Real;

          now

            let x be VECTOR of X;

            

             A8: |.((u1 . x) + (v1 . x)).| <= ( |.(u1 . x).| + |.(v1 . x).|) by COMPLEX1: 56;

            

             A9: |.(v1 . x).| <= (K2 * ||.x.||) by A5;

             |.(u1 . x).| <= (K1 * ||.x.||) by A7;

            then

             A10: ( |.(u1 . x).| + |.(v1 . x).|) <= ((K1 * ||.x.||) + (K2 * ||.x.||)) by A9, XREAL_1: 7;

             |.(f . x).| = |.((u1 . x) + (v1 . x)).| by DUALSP01: 12;

            hence |.(f . x).| <= (K3 * ||.x.||) by A8, A10, XXREAL_0: 2;

          end;

          hence thesis by A4, A6, BHSP_6:def 4;

        end;

        hence thesis by Def10;

      end;

      for a be Real, v be VECTOR of (X *' ) st v in W holds (a * v) in W

      proof

        let a be Real;

        let v be VECTOR of (X *' ) such that

         A11: v in W;

        reconsider f = (a * v) as linear-Functional of X by DUALSP01:def 6;

        f is Lipschitzian

        proof

          reconsider v1 = v as Lipschitzian linear-Functional of X by A11, Def10;

          consider K be Real such that

           A12: 0 < K and

           A13: for x be Point of X holds |.(v1 . x).| <= (K * ||.x.||) by BHSP_6:def 4;

          

           B12: 0 <= |.a.| by COMPLEX1: 46;

          ( |.a.| + 0 ) < ( |.a.| + 1) by XREAL_1: 8;

          then

           B2: ( |.a.| * K) <= (( |.a.| + 1) * K) by A12, XREAL_1: 64;

          now

            let x be VECTOR of X;

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

            then

             A15: ( |.a.| * |.(v1 . x).|) <= ( |.a.| * (K * ||.x.||)) by A13, XREAL_1: 64;

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

            then

             A16: |.(f . x).| <= ( |.a.| * (K * ||.x.||)) by A15, DUALSP01: 13;

             0 <= ||.x.|| by BHSP_1: 28;

            then (( |.a.| * K) * ||.x.||) <= ((( |.a.| + 1) * K) * ||.x.||) by B2, XREAL_1: 64;

            hence |.(f . x).| <= ((( |.a.| + 1) * K) * ||.x.||) by A16, XXREAL_0: 2;

          end;

          hence thesis by B12, A12, BHSP_6:def 4;

        end;

        hence thesis by Def10;

      end;

      hence thesis by A1;

    end;

    registration

      let X be RealUnitarySpace;

      cluster ( BoundedLinearFunctionals X) -> non empty linearly-closed;

      coherence

      proof

        set f = the Lipschitzian linear-Functional of X;

        f in ( BoundedLinearFunctionals X) by Def10;

        hence thesis by Th17;

      end;

    end

    definition

      let X be RealUnitarySpace;

      let f be object;

      :: DUALSP04:def9

      func Bound2Lipschitz (f,X) -> Lipschitzian linear-Functional of X equals ( In (f,( BoundedLinearFunctionals X)));

      coherence by Def10;

    end

    definition

      let X be RealUnitarySpace;

      let u be linear-Functional of X;

      :: DUALSP04:def10

      func PreNorms u -> non empty Subset of REAL equals { |.(u . t).| where t be VECTOR of X : ||.t.|| <= 1 };

      coherence

      proof

         A1:

        now

          let x be object;

          now

            assume x in { |.(u . t).| where t be VECTOR of X : ||.t.|| <= 1 };

            then ex t be VECTOR of X st x = |.(u . t).| & ||.t.|| <= 1;

            hence x in REAL by XREAL_0:def 1;

          end;

          hence x in { |.(u . t).| where t be VECTOR of X : ||.t.|| <= 1 } implies x in REAL ;

        end;

         ||.( 0. X).|| = 0 by SQUARE_1: 17, BHSP_1: 1;

        then |.(u . ( 0. X)).| in { |.(u . t).| where t be VECTOR of X : ||.t.|| <= 1 };

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    

     Th27X: for X be RealUnitarySpace, g be Lipschitzian linear-Functional of X holds ( PreNorms g) is bounded_above

    proof

      let X be RealUnitarySpace;

      let g be Lipschitzian linear-Functional of X;

      consider K be Real such that

       A1: 0 < K & for x be VECTOR of X holds |.(g . x).| <= (K * ||.x.||) by BHSP_6:def 4;

      take K;

      let r be ExtReal;

      assume r in ( PreNorms g);

      then

      consider t be VECTOR of X such that

       A3: r = |.(g . t).| & ||.t.|| <= 1;

      

       A5: |.(g . t).| <= (K * ||.t.||) by A1;

      (K * ||.t.||) <= (K * 1) by A1, A3, XREAL_1: 64;

      hence r <= K by A3, A5, XXREAL_0: 2;

    end;

    registration

      let X be RealUnitarySpace, g be Lipschitzian linear-Functional of X;

      cluster ( PreNorms g) -> bounded_above;

      coherence by Th27X;

    end

    definition

      let X be RealUnitarySpace;

      :: DUALSP04:def11

      func BoundedLinearFunctionalsNorm X -> Function of ( BoundedLinearFunctionals X), REAL means

      : Def14: for x be object st x in ( BoundedLinearFunctionals X) holds (it . x) = ( upper_bound ( PreNorms ( Bound2Lipschitz (x,X))));

      existence

      proof

        deffunc F( object) = ( upper_bound ( PreNorms ( Bound2Lipschitz ($1,X))));

        

         A1: for z be object st z in ( BoundedLinearFunctionals X) holds F(z) in REAL by XREAL_0:def 1;

        thus ex f be Function of ( BoundedLinearFunctionals X), REAL st for x be object st x in ( BoundedLinearFunctionals X) holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

      end;

      uniqueness

      proof

        let NORM1,NORM2 be Function of ( BoundedLinearFunctionals X), REAL such that

         A2: for x be object st x in ( BoundedLinearFunctionals X) holds (NORM1 . x) = ( upper_bound ( PreNorms ( Bound2Lipschitz (x,X)))) and

         A3: for x be object st x in ( BoundedLinearFunctionals X) holds (NORM2 . x) = ( upper_bound ( PreNorms ( Bound2Lipschitz (x,X))));

        for z be object st z in ( BoundedLinearFunctionals X) holds (NORM1 . z) = (NORM2 . z)

        proof

          let z be object such that

           A5: z in ( BoundedLinearFunctionals X);

          (NORM1 . z) = ( upper_bound ( PreNorms ( Bound2Lipschitz (z,X)))) by A2, A5;

          hence thesis by A3, A5;

        end;

        hence thesis;

      end;

    end

    

     Th23: for X be RealUnitarySpace, f be Lipschitzian linear-Functional of X holds ( Bound2Lipschitz (f,X)) = f

    proof

      let X be RealUnitarySpace;

      let f be Lipschitzian linear-Functional of X;

      f in ( BoundedLinearFunctionals X) by Def10;

      hence thesis by SUBSET_1:def 8;

    end;

    registration

      let X be RealUnitarySpace;

      let f be Lipschitzian linear-Functional of X;

      reduce ( Bound2Lipschitz (f,X)) to f;

      reducibility by Th23;

    end

    theorem :: DUALSP04:16

    

     Th24: for X be RealUnitarySpace, f be Lipschitzian linear-Functional of X holds (( BoundedLinearFunctionalsNorm X) . f) = ( upper_bound ( PreNorms f))

    proof

      let X be RealUnitarySpace;

      let f be Lipschitzian linear-Functional of X;

      reconsider f9 = f as set;

      

      thus (( BoundedLinearFunctionalsNorm X) . f) = ( upper_bound ( PreNorms ( Bound2Lipschitz (f9,X)))) by Def14

      .= ( upper_bound ( PreNorms f));

    end;

    definition

      let X be RealUnitarySpace;

      :: DUALSP04:def12

      func DualSp X -> non empty NORMSTR equals NORMSTR (# ( BoundedLinearFunctionals X), ( Zero_ (( BoundedLinearFunctionals X),(X *' ))), ( Add_ (( BoundedLinearFunctionals X),(X *' ))), ( Mult_ (( BoundedLinearFunctionals X),(X *' ))), ( BoundedLinearFunctionalsNorm X) #);

      coherence ;

    end

    theorem :: DUALSP04:17

    

     Th26: for X be RealUnitarySpace, f be Point of ( DualSp X), g be Lipschitzian linear-Functional of X st g = f holds for t be VECTOR of X holds |.(g . t).| <= ( ||.f.|| * ||.t.||)

    proof

      let X be RealUnitarySpace;

      let f be Point of ( DualSp X);

      let g be Lipschitzian linear-Functional of X such that

       A1: g = f;

      let t be VECTOR of X;

      per cases ;

        suppose

         A3: t = ( 0. X);

        then

         A4: ||.t.|| = 0 by BHSP_1: 26;

        (g . t) = (g . ( 0 * ( 0. X))) by A3

        .= ( 0 * (g . ( 0. X))) by HAHNBAN:def 3

        .= 0 ;

        hence |.(g . t).| <= ( ||.f.|| * ||.t.||) by A4, COMPLEX1: 44;

      end;

        suppose

         A5: t <> ( 0. X);

        reconsider t1 = (( ||.t.|| " ) * t) as VECTOR of X;

        

         A6: ||.t.|| <> 0 by A5, BHSP_1: 26;

        then

         B61: 0 < ||.t.|| by BHSP_1: 28;

        

         A7: |.( ||.t.|| " ).| = |.(1 * ( ||.t.|| " )).|

        .= |.(1 / ||.t.||).| by XCMPLX_0:def 9

        .= (1 / ||.t.||) by B61, ABSVALUE:def 1

        .= (1 * ( ||.t.|| " )) by XCMPLX_0:def 9

        .= ( ||.t.|| " );

        

         A8: ( |.(g . t).| / ||.t.||) = ( |.(g . t).| * ( ||.t.|| " )) by XCMPLX_0:def 9

        .= |.(( ||.t.|| " ) * (g . t)).| by A7, COMPLEX1: 65

        .= |.(g . t1).| by HAHNBAN:def 3;

         ||.t1.|| = ( |.( ||.t.|| " ).| * ||.t.||) by BHSP_1: 27

        .= 1 by A6, A7, XCMPLX_0:def 7;

        then ( |.(g . t).| / ||.t.||) in { |.(g . s).| where s be VECTOR of X : ||.s.|| <= 1 } by A8;

        then ( |.(g . t).| / ||.t.||) <= ( upper_bound ( PreNorms g)) by SEQ_4:def 1;

        then

         A9: ( |.(g . t).| / ||.t.||) <= ||.f.|| by A1, Th24;

        

         A10: (( |.(g . t).| / ||.t.||) * ||.t.||) = (( |.(g . t).| * ( ||.t.|| " )) * ||.t.||) by XCMPLX_0:def 9

        .= ( |.(g . t).| * (( ||.t.|| " ) * ||.t.||))

        .= ( |.(g . t).| * 1) by A6, XCMPLX_0:def 7

        .= |.(g . t).|;

         0 <= ||.t.|| by BHSP_1: 28;

        hence |.(g . t).| <= ( ||.f.|| * ||.t.||) by A9, A10, XREAL_1: 64;

      end;

    end;

    theorem :: DUALSP04:18

    

     Th27: for X be RealUnitarySpace, f be Point of ( DualSp X) holds 0 <= ||.f.||

    proof

      let X be RealUnitarySpace;

      let f be Point of ( DualSp X);

      reconsider g = f as Lipschitzian linear-Functional of X by Def10;

      consider r0 be object such that

       A1: r0 in ( PreNorms g) by XBOOLE_0:def 1;

      reconsider r0 as Real by A1;

      

       A3: (( BoundedLinearFunctionalsNorm X) . f) = ( upper_bound ( PreNorms g)) by Th24;

      now

        let r be Real;

        assume r in ( PreNorms g);

        then ex t be VECTOR of X st r = |.(g . t).| & ||.t.|| <= 1;

        hence 0 <= r by COMPLEX1: 46;

      end;

      then 0 <= r0 by A1;

      hence thesis by A1, SEQ_4:def 1, A3;

    end;

    theorem :: DUALSP04:19

    

     LM6A: for X be RealUnitarySpace, f be Function of X, REAL , g be Function of ( RUSp2RNSp X), REAL st f = g holds f is additive homogeneous iff g is additive homogeneous

    proof

      let X be RealUnitarySpace, f be Function of X, REAL , g be Function of ( RUSp2RNSp X), REAL ;

      assume

       AS: f = g;

      set Y = ( RUSp2RNSp X);

      hereby

        assume

         AS1: f is additive homogeneous;

        

         A1: g is additive

        proof

          let x,y be Point of Y;

          reconsider x1 = x, y1 = y as Point of X;

          

          thus (g . (x + y)) = (f . (x1 + y1)) by AS

          .= ((g . x) + (g . y)) by AS, AS1, HAHNBAN:def 2;

        end;

        g is homogeneous

        proof

          let x be Point of Y, r be Real;

          reconsider x1 = x as Point of X;

          

          thus (g . (r * x)) = (f . (r * x1)) by AS

          .= (r * (g . x)) by AS, AS1, HAHNBAN:def 3;

        end;

        hence g is additive homogeneous by A1;

      end;

      assume

       AS2: g is additive homogeneous;

      

       A2: f is additive

      proof

        let x,y be Point of X;

        reconsider x1 = x, y1 = y as Point of Y;

        

        thus (f . (x + y)) = (g . (x1 + y1)) by AS

        .= ((f . x) + (f . y)) by AS, AS2, HAHNBAN:def 2;

      end;

      f is homogeneous

      proof

        let x be Point of X, r be Real;

        reconsider x1 = x as Point of Y;

        

        thus (f . (r * x)) = (g . (r * x1)) by AS

        .= (r * (f . x)) by AS, AS2, HAHNBAN:def 3;

      end;

      hence f is additive homogeneous by A2;

    end;

    theorem :: DUALSP04:20

    

     LM6B: for X be RealUnitarySpace, f be linear-Functional of X, g be linear-Functional of ( RUSp2RNSp X) st f = g holds f is Lipschitzian iff g is Lipschitzian

    proof

      let X be RealUnitarySpace, f be linear-Functional of X, g be linear-Functional of ( RUSp2RNSp X);

      assume

       AS: f = g;

      set Y = ( RUSp2RNSp X);

      hereby

        assume f is Lipschitzian;

        then

        consider K be Real such that

         A1: 0 < K & for x be Point of X holds |.(f . x).| <= (K * ||.x.||) by BHSP_6:def 4;

        for y be Point of Y holds |.(g . y).| <= (K * ||.y.||)

        proof

          let y be Point of Y;

          reconsider x = y as Point of X;

           ||.y.|| = ||.x.|| by Def1;

          hence |.(g . y).| <= (K * ||.y.||) by A1, AS;

        end;

        hence g is Lipschitzian by A1;

      end;

      assume g is Lipschitzian;

      then

      consider K be Real such that

       A2: 0 <= K & for y be Point of Y holds |.(g . y).| <= (K * ||.y.||);

      

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

      for x be Point of X holds |.(f . x).| <= ((K + 1) * ||.x.||)

      proof

        let x be Point of X;

        reconsider y = x as Point of Y;

         ||.x.|| = ||.y.|| by Def1;

        then

         B3: |.(f . x).| <= (K * ||.x.||) by A2, AS;

         0 <= ||.x.|| by BHSP_1: 28;

        then (K * ||.x.||) <= ((K + 1) * ||.x.||) by A4, XREAL_1: 64;

        hence |.(f . x).| <= ((K + 1) * ||.x.||) by B3, XXREAL_0: 2;

      end;

      hence f is Lipschitzian by A2, BHSP_6:def 4;

    end;

    theorem :: DUALSP04:21

    

     LM6: for X be RealUnitarySpace holds ( BoundedLinearFunctionals X) = ( BoundedLinearFunctionals ( RUSp2RNSp X))

    proof

      let X be RealUnitarySpace;

      set Y = ( RUSp2RNSp X);

      now

        let x be object;

        assume x in ( BoundedLinearFunctionals X);

        then

         A1: x is Lipschitzian linear-Functional of X by Def10;

        then x is linear-Functional of Y by LM6A;

        then x is Lipschitzian linear-Functional of Y by A1, LM6B;

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

      end;

      then

       A2: ( BoundedLinearFunctionals X) c= ( BoundedLinearFunctionals Y);

      now

        let x be object;

        assume x in ( BoundedLinearFunctionals Y);

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

        then x is Lipschitzian linear-Functional of X by LM6B, LM6A;

        hence x in ( BoundedLinearFunctionals X) by Def10;

      end;

      then ( BoundedLinearFunctionals Y) c= ( BoundedLinearFunctionals X);

      hence thesis by A2;

    end;

    theorem :: DUALSP04:22

    

     LM8: for X be RealUnitarySpace, u be linear-Functional of X, v be linear-Functional of ( RUSp2RNSp X) st u = v holds ( PreNorms u) = ( PreNorms v)

    proof

      let X be RealUnitarySpace, u be linear-Functional of X, v be linear-Functional of ( RUSp2RNSp X);

      assume

       AS: u = v;

      set Y = ( RUSp2RNSp X);

       A11:

      now

        let x be object;

        assume

         AS1: x in ( PreNorms u);

        then

        reconsider y = x as Real;

        consider t be VECTOR of X such that

         B1: y = |.(u . t).| & ||.t.|| <= 1 by AS1;

        reconsider t1 = t as VECTOR of Y;

         ||.t1.|| <= 1 by B1, Def1;

        hence x in ( PreNorms v) by AS, B1;

      end;

      now

        let x be object;

        assume

         AS2: x in ( PreNorms v);

        then

        reconsider y = x as Real;

        consider t be VECTOR of Y such that

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

        reconsider t1 = t as VECTOR of X;

         ||.t1.|| <= 1 by B1, Def1;

        hence x in ( PreNorms u) by AS, B1;

      end;

      hence ( PreNorms u) = ( PreNorms v) by A11;

    end;

    theorem :: DUALSP04:23

    

     LM9: for X be RealUnitarySpace holds ( BoundedLinearFunctionalsNorm X) = ( BoundedLinearFunctionalsNorm ( RUSp2RNSp X))

    proof

      let X be RealUnitarySpace;

      set Y = ( RUSp2RNSp X);

      set f = ( BoundedLinearFunctionalsNorm X);

      set g = ( BoundedLinearFunctionalsNorm Y);

      

       A1: ( dom f) = ( BoundedLinearFunctionals X) by FUNCT_2:def 1

      .= ( BoundedLinearFunctionals Y) by LM6

      .= ( dom g) by FUNCT_2:def 1;

      now

        let x be object;

        assume

         B11: x in ( dom f);

        then

         B1: x in ( BoundedLinearFunctionals X);

        

         B2: (f . x) = ( upper_bound ( PreNorms ( Bound2Lipschitz (x,X)))) by B11, Def14;

        

         B31: x in ( BoundedLinearFunctionals Y) by B1, LM6;

        ( Bound2Lipschitz (x,X)) = ( Bound2Lipschitz (x,( RUSp2RNSp X))) by LM6;

        then ( upper_bound ( PreNorms ( Bound2Lipschitz (x,X)))) = ( upper_bound ( PreNorms ( Bound2Lipschitz (x,Y)))) by LM8;

        hence (f . x) = (g . x) by B2, B31, DUALSP01:def 14;

      end;

      hence thesis by A1;

    end;

    theorem :: DUALSP04:24

    

     LM10A: for X be RealUnitarySpace holds ( LinearFunctionals X) = ( LinearFunctionals ( RUSp2RNSp X))

    proof

      let X be RealUnitarySpace;

      set Y = ( RUSp2RNSp X);

      now

        let x be object;

        assume x in ( LinearFunctionals X);

        then x is linear-Functional of X by DUALSP01:def 6;

        then x is linear-Functional of Y by LM6A;

        hence x in ( LinearFunctionals Y) by DUALSP01:def 6;

      end;

      then

       A1: ( LinearFunctionals X) c= ( LinearFunctionals Y);

      now

        let x be object;

        assume x in ( LinearFunctionals Y);

        then x is linear-Functional of Y by DUALSP01:def 6;

        then x is linear-Functional of X by LM6A;

        hence x in ( LinearFunctionals X) by DUALSP01:def 6;

      end;

      then ( LinearFunctionals Y) c= ( LinearFunctionals X);

      hence thesis by A1;

    end;

    theorem :: DUALSP04:25

    

     LM10B: for X be RealUnitarySpace holds (X *' ) = (( RUSp2RNSp X) *' )

    proof

      let X be RealUnitarySpace;

      set Y = ( RUSp2RNSp X);

      the carrier of (X *' ) = the carrier of (Y *' ) by LM10A;

      hence (X *' ) = (( RUSp2RNSp X) *' );

    end;

    theorem :: DUALSP04:26

    for X be RealUnitarySpace holds ( DualSp X) = ( DualSp ( RUSp2RNSp X))

    proof

      let X be RealUnitarySpace;

      set Y = ( RUSp2RNSp X);

      set X1 = ( BoundedLinearFunctionals X);

      set Y1 = ( BoundedLinearFunctionals Y);

      

       A0: the carrier of (X *' ) = the carrier of (Y *' ) by LM10B;

      

       A2: the ZeroF of ( DualSp X) = ( 0. (X *' )) by RSSPACE:def 10

      .= ( 0. (Y *' )) by LM10B

      .= the ZeroF of ( DualSp Y) by DUALSP01: 17, RSSPACE:def 10;

      

       A3: the addF of ( DualSp X) = (the addF of (X *' ) || X1) by RSSPACE:def 8

      .= (the addF of (Y *' ) || Y1) by LM6, A0

      .= the addF of ( DualSp Y) by DUALSP01: 17, RSSPACE:def 8;

      

       A4: the Mult of ( DualSp X) = (the Mult of (X *' ) | [: REAL , X1:]) by RSSPACE:def 9

      .= (the Mult of (Y *' ) | [: REAL , Y1:]) by LM6, A0

      .= the Mult of ( DualSp Y) by DUALSP01: 17, RSSPACE:def 9;

      the normF of ( DualSp X) = the normF of ( DualSp Y) by LM9;

      hence ( DualSp X) = ( DualSp ( RUSp2RNSp X)) by A2, A3, A4;

    end;

    begin

    theorem :: DUALSP04:27

    for X be RealUnitarySpace, M,N be Subspace of X st the carrier of M c= the carrier of N holds the carrier of ( Ort_Comp N) c= the carrier of ( Ort_Comp M)

    proof

      let X be RealUnitarySpace;

      let M,N be Subspace of X;

      assume

       A1: the carrier of M c= the carrier of N;

      let x be object;

      assume x in the carrier of ( Ort_Comp N);

      then x in { v where v be VECTOR of X : for w be VECTOR of X st w in N holds (w,v) are_orthogonal } by RUSUB_5:def 3;

      then

       A2: ex v1 be VECTOR of X st x = v1 & for w be VECTOR of X st w in N holds (w,v1) are_orthogonal ;

      then

      reconsider x as VECTOR of X;

      for y be VECTOR of X st y in M holds (y,x) are_orthogonal

      proof

        let y be VECTOR of X;

        assume y in M;

        then y in N by A1;

        hence (y,x) are_orthogonal by A2;

      end;

      then x in { v where v be VECTOR of X : for w be VECTOR of X st w in M holds (w,v) are_orthogonal };

      hence thesis by RUSUB_5:def 3;

    end;

    theorem :: DUALSP04:28

    for X be RealUnitarySpace, M be Subspace of X holds the carrier of M c= the carrier of ( Ort_Comp ( Ort_Comp M))

    proof

      let X be RealUnitarySpace;

      let M be Subspace of X;

      let x be object;

      assume

       AS: x in the carrier of M;

      then

       A1: x in M;

      the carrier of M c= the carrier of X by RUSUB_1:def 1;

      then

      reconsider x as VECTOR of X by AS;

      for y be VECTOR of X st y in ( Ort_Comp M) holds (x,y) are_orthogonal

      proof

        let y be VECTOR of X;

        assume y in ( Ort_Comp M);

        then y in { v where v be VECTOR of X : for w be VECTOR of X st w in M holds (w,v) are_orthogonal } by RUSUB_5:def 3;

        then ex v be VECTOR of X st y = v & for w be VECTOR of X st w in M holds (w,v) are_orthogonal ;

        hence thesis by A1;

      end;

      then x in { v where v be VECTOR of X : for w be VECTOR of X st w in ( Ort_Comp M) holds (w,v) are_orthogonal };

      hence thesis by RUSUB_5:def 3;

    end;

    theorem :: DUALSP04:29

    

     Lm814: for X be RealUnitarySpace, M be Subspace of X, x be Point of X st x in (the carrier of M /\ the carrier of ( Ort_Comp M)) holds x = ( 0. X)

    proof

      let X be RealUnitarySpace, M be Subspace of X, x be Point of X;

      assume x in (the carrier of M /\ the carrier of ( Ort_Comp M));

      then

       A1: x in M & x in ( Ort_Comp M) by XBOOLE_0:def 4;

      then x in { v where v be VECTOR of X : for w be VECTOR of X st w in M holds (w,v) are_orthogonal } by RUSUB_5:def 3;

      then

      consider v be VECTOR of X such that

       A2: x = v & for w be VECTOR of X st w in M holds (w,v) are_orthogonal ;

      (x,x) are_orthogonal by A1, A2;

      hence thesis by BHSP_1:def 2;

    end;

    theorem :: DUALSP04:30

    for X be RealUnitarySpace, M be Subspace of X, N be non empty Subset of X st N = the carrier of ( Ort_Comp M) holds N is linearly-closed & N is closed

    proof

      let X be RealUnitarySpace, M be Subspace of X, N be non empty Subset of X;

      assume

       AS1: N = the carrier of ( Ort_Comp M);

      hence N is linearly-closed by RUSUB_1: 28;

      for s be sequence of X st ( rng s) c= N & s is convergent holds ( lim s) in N

      proof

        let s be sequence of X;

        assume

         AS2: ( rng s) c= N & s is convergent;

         A1:

        now

          let i be Nat;

          (s . i) in ( rng s) by FUNCT_2: 4, ORDINAL1:def 12;

          then (s . i) in N by AS2;

          then (s . i) in { v where v be VECTOR of X : for w be VECTOR of X st w in M holds (w,v) are_orthogonal } by AS1, RUSUB_5:def 3;

          then

          consider v be VECTOR of X such that

           B1: v = (s . i) & for w be VECTOR of X st w in M holds (w,v) are_orthogonal ;

          thus for w be VECTOR of X st w in M holds (w .|. (s . i)) = 0 by B1, BHSP_1:def 3;

        end;

        for w be VECTOR of X st w in M holds (w .|. ( lim s)) = 0

        proof

          let w be VECTOR of X;

          assume

           AS3: w in M;

          reconsider g = (w .|. ( lim s)) as Real;

          for p be Real st 0 < p holds ex m be Nat st for n be Nat st m <= n holds |.((( seq_const 0 ) . n) - (w .|. ( lim s))).| < p

          proof

            let p be Real;

            assume

             B0: 0 < p;

            

             B1: 0 <= ||.w.|| by BHSP_1: 28;

            reconsider r = (p / ( ||.w.|| + 1)) as Real;

            

             B41: ( ||.w.|| + 0 ) < ( ||.w.|| + 1) by XREAL_1: 8;

            (r * ( ||.w.|| + 1)) = p by B1, XCMPLX_1: 87;

            then

             B5: 0 < r & (r * ||.w.||) < p by B0, B1, B41, XREAL_1: 68;

            consider m be Nat such that

             B6: for n be Nat st m <= n holds ||.((s . n) - ( lim s)).|| < r by B1, B0, AS2, BHSP_2: 19;

            

             B7: for n be Nat st m <= n holds |.((( seq_const 0 ) . n) - (w .|. ( lim s))).| < p

            proof

              let n be Nat;

              assume m <= n;

              then

               C1: ||.((s . n) - ( lim s)).|| < r by B6;

              

               C2: |.((w .|. (s . n)) - (w .|. ( lim s))).| = |.(w .|. ((s . n) - ( lim s))).| by BHSP_1: 12;

              

               C3: |.(w .|. ((s . n) - ( lim s))).| <= ( ||.w.|| * ||.((s . n) - ( lim s)).||) by BHSP_1: 29;

              ( ||.w.|| * ||.((s . n) - ( lim s)).||) <= ( ||.w.|| * r) by B1, C1, XREAL_1: 64;

              then

               C41: |.((w .|. (s . n)) - (w .|. ( lim s))).| <= ( ||.w.|| * r) by C2, C3, XXREAL_0: 2;

              (w .|. (s . n)) = 0 by A1, AS3

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

              hence thesis by C41, B5, XXREAL_0: 2;

            end;

            take m;

            thus thesis by B7;

          end;

          then ( lim ( seq_const 0 )) = (w .|. ( lim s)) by SEQ_2:def 7;

          then (( seq_const 0 ) . 0 ) = (w .|. ( lim s)) by SEQ_4: 26;

          hence (w .|. ( lim s)) = 0 ;

        end;

        then

         A3: for w be VECTOR of X st w in M holds (w,( lim s)) are_orthogonal ;

        reconsider v = ( lim s) as VECTOR of X;

        ( lim s) in { v where v be VECTOR of X : for w be VECTOR of X st w in M holds (w,v) are_orthogonal } by A3;

        hence ( lim s) in N by AS1, RUSUB_5:def 3;

      end;

      hence N is closed by LM1;

    end;

    

     Lm88A: for X be RealUnitarySpace, x,y be Point of X holds (( ||.(x + y).|| * ||.(x + y).||) + ( ||.(x - y).|| * ||.(x - y).||)) = ((2 * ( ||.x.|| * ||.x.||)) + (2 * ( ||.y.|| * ||.y.||)))

    proof

      let X be RealUnitarySpace, x,y be Point of X;

      ( ||.(x + y).|| ^2 ) = ( ||.(x + y).|| * ||.(x + y).||) & ( ||.(x - y).|| ^2 ) = ( ||.(x - y).|| * ||.(x - y).||) & ( ||.x.|| ^2 ) = ( ||.x.|| * ||.x.||) & ( ||.y.|| ^2 ) = ( ||.y.|| * ||.y.||) by SQUARE_1:def 1;

      hence thesis by RUSUB_5: 31;

    end;

    theorem :: DUALSP04:31

    

     Lm88: for X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X, d be Real st N = the carrier of M & N is closed & (ex Y be non empty Subset of REAL st Y = { ||.(x - y).|| where y be Point of X : y in M } & d = ( lower_bound Y) >= 0 ) holds ex x0 be Point of X st d = ||.(x - x0).|| & x0 in M

    proof

      let X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X, d be Real;

      assume that

       A1: N = the carrier of M & N is closed and

       A2: ex Y be non empty Subset of REAL st Y = { ||.(x - y).|| where y be Point of X : y in M } & d = ( lower_bound Y) >= 0 ;

      consider Y be non empty Subset of REAL such that

       A3: Y = { ||.(x - y).|| where y be Point of X : y in M } & d = ( lower_bound Y) >= 0 by A2;

      reconsider r0 = 0 as Real;

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

      proof

        let r be ExtReal;

        assume r in Y;

        then ex y be Point of X st r = ||.(x - y).|| & y in M by A3;

        hence r0 <= r by BHSP_1: 28;

      end;

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

      then

       A4: Y is bounded_below;

      defpred P[ Nat, Real] means $2 in Y & $2 < (d + (1 / ($1 + 1)));

      

       F1: for n be Element of NAT holds ex r be Element of REAL st P[n, r]

      proof

        let n be Element of NAT ;

        reconsider n1 = n as Nat;

        consider r1 be Real such that

         F11: r1 in Y & r1 < (d + (1 / (n1 + 1))) by A4, A3, SEQ_4:def 2;

        reconsider r = r1 as Element of REAL by XREAL_0:def 1;

        take r;

        thus thesis by F11;

      end;

      consider S be Function of NAT , REAL such that

       B3: for n be Element of NAT holds P[n, (S . n)] from FUNCT_2:sch 3( F1);

      

       B4: for n be Nat holds |.((S . n) - d).| <= (1 / (n + 1))

      proof

        let n be Nat;

        

         C11: n in NAT by ORDINAL1:def 12;

        then (S . n) in Y & (S . n) < (d + (1 / (n + 1))) by B3;

        then

         C21: d <= (S . n) by A4, A3, SEQ_4:def 2;

        ((S . n) - d) < ((d + (1 / (n + 1))) - d) by C11, B3, XREAL_1: 9;

        hence |.((S . n) - d).| <= (1 / (n + 1)) by C21, ABSVALUE:def 1, XREAL_1: 48;

      end;

      

       B5: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((S . m) - d).| < p

      proof

        let p be Real;

        assume

         D0: 0 < p;

        reconsider r = (1 / p) as Real;

        consider n be Nat such that

         E1: r < n by SEQ_4: 3;

        (r * p) = 1 by D0, XCMPLX_1: 106;

        then

         E3: 1 < (n * p) by D0, E1, XREAL_1: 68;

        (n * p) < ((n + 1) * p) by D0, XREAL_1: 68, NAT_1: 16;

        then

         E4: 1 < ((n + 1) * p) by E3, XXREAL_0: 2;

        

         D1: (1 / (n + 1)) < p by E4, XREAL_1: 83;

        take n;

        let m be Nat;

        assume n <= m;

        then

         D21: (n + 1) <= (m + 1) by XREAL_1: 6;

        ((m + 1) " ) = (1 / (m + 1)) & ((n + 1) " ) = (1 / (n + 1)) by XCMPLX_1: 215;

        then (1 / (m + 1)) <= (1 / (n + 1)) by D21, XREAL_1: 85;

        then

         D3: (1 / (m + 1)) < p by XXREAL_0: 2, D1;

         |.((S . m) - d).| <= (1 / (m + 1)) by B4;

        hence |.((S . m) - d).| < p by D3, XXREAL_0: 2;

      end;

      then

       A5: S is convergent;

      then

       A6: ( lim S) = d by SEQ_2:def 7, B5;

      defpred P1[ Nat, Point of X] means $2 in M & (S . $1) = ||.(x - $2).||;

      

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

      proof

        let n be Element of NAT ;

        (S . n) in Y & (S . n) < (d + (1 / (n + 1))) by B3;

        then

        consider y be Point of X such that

         F21: (S . n) = ||.(x - y).|| & y in M by A3;

        take y;

        thus thesis by F21;

      end;

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

       A7: for n be Element of NAT holds P1[n, (z . n)] from FUNCT_2:sch 3( F2);

      for n be Nat holds (z . n) in M & (S . n) = ||.(x - (z . n)).||

      proof

        let n be Nat;

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

        (z . n1) in M & (S . n1) = ||.(x - (z . n1)).|| by A7;

        hence thesis;

      end;

      then

      consider z be sequence of X such that

       A8: for n be Nat holds (z . n) in M & (S . n) = ||.(x - (z . n)).||;

      reconsider S1 = (S (#) S), S2 = (S (#) S) as Real_Sequence;

      reconsider SA = (2 (#) S1), SB = (2 (#) S2) as Real_Sequence;

      

       C3: ( lim S1) = (d * d) by A6, A5, SEQ_2: 15;

      

       C4: ( lim S2) = (d * d) by A6, A5, SEQ_2: 15;

      

       C5: ( lim SA) = (2 * (d * d)) by C3, A5, SEQ_2: 8;

      

       C6: ( lim SB) = (2 * (d * d)) by C4, A5, SEQ_2: 8;

      

       A12: for e be Real st 0 < e holds ex k be Nat st for n,m be Nat st n >= k & m >= k holds |.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e

      proof

        let e be Real;

        assume

         B01: 0 < e;

        then

        consider k1 be Nat such that

         B1: for n be Nat st n >= k1 holds |.((SA . n) - (2 * (d * d))).| < (e / 2) by A5, C5, SEQ_2:def 7;

        consider k2 be Nat such that

         B2: for m be Nat st m >= k2 holds |.((SB . m) - (2 * (d * d))).| < (e / 2) by B01, A5, C6, SEQ_2:def 7;

        ( max (k1,k2)) is natural;

        then

        reconsider k = ( max (k1,k2)) as Nat;

        

         B3: for n,m be Nat st n >= k & m >= k holds |.(((SA . m) + (SB . n)) - (4 * (d * d))).| < e

        proof

          let n,m be Nat;

          assume

           AS: n >= k & m >= k;

          k >= k1 & k >= k2 by XXREAL_0: 25;

          then

           C0: n >= k1 & m >= k2 by AS, XXREAL_0: 2;

          then

           C1: |.((SA . n) - (2 * (d * d))).| < (e / 2) by B1;

          

           C2: |.((SB . m) - (2 * (d * d))).| < (e / 2) by C0, B2;

          

           C4: |.(((SA . n) - (2 * (d * d))) + ((SB . m) - (2 * (d * d)))).| <= ( |.((SA . n) - (2 * (d * d))).| + |.((SB . m) - (2 * (d * d))).|) by COMPLEX1: 56;

          ( |.((SA . n) - (2 * (d * d))).| + |.((SB . m) - (2 * (d * d))).|) < ((e / 2) + (e / 2)) by C1, C2, XREAL_1: 8;

          hence thesis by C4, XXREAL_0: 2;

        end;

        take k;

        thus thesis by B3;

      end;

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

      proof

        let p be Real;

        assume

         AS1: p > 0 ;

        then

        consider k be Nat such that

         D1: for n,m be Nat st n >= k & m >= k holds |.(((SA . m) + (SB . n)) - (4 * (d * d))).| < (p * p) by A12;

        

         D2: for n,m be Nat st n >= k & m >= k holds ||.((z . n) - (z . m)).|| < p

        proof

          let n,m be Nat;

          assume n >= k & m >= k;

          then

           B0: |.(((SA . m) + (SB . n)) - (4 * (d * d))).| < (p * p) by D1;

          set C = ||.(x - (z . n)).||;

          set D = ||.(x - (z . m)).||;

          

           B2: ((x - (z . n)) + (x - (z . m))) = (((( - (z . n)) + x) + x) + ( - (z . m))) by RLVECT_1:def 3

          .= (((x + x) + ( - (z . n))) + ( - (z . m))) by RLVECT_1:def 3

          .= ((x + x) + (( - (z . n)) + ( - (z . m)))) by RLVECT_1:def 3

          .= ((x + x) + ( - ((z . n) + (z . m)))) by RLVECT_1: 31

          .= (((1 * x) + x) + ( - ((z . n) + (z . m)))) by RLVECT_1:def 8

          .= (((1 * x) + (1 * x)) + ( - ((z . n) + (z . m)))) by RLVECT_1:def 8

          .= (((1 + 1) * x) + ( - ((z . n) + (z . m)))) by RLVECT_1:def 6

          .= ((2 * x) - ((z . n) + (z . m)));

          

           B3: ((x - (z . n)) - (x - (z . m))) = ((x + ( - (z . n))) + ((z . m) + ( - x))) by RLVECT_1: 33

          .= (( - x) + ((x + ( - (z . n))) + (z . m))) by RLVECT_1:def 3

          .= (( - x) + (x + (( - (z . n)) + (z . m)))) by RLVECT_1:def 3

          .= ((( - x) + x) + (( - (z . n)) + (z . m))) by RLVECT_1:def 3

          .= (( 0. X) + (( - (z . n)) + (z . m))) by RLVECT_1: 5

          .= ((z . m) - (z . n));

          set E = ||.((2 * x) - ((z . n) + (z . m))).||;

          set F = ||.((z . m) - (z . n)).||;

          

           B6: (F * F) = (((E * E) + (F * F)) + ( - (E * E)))

          .= (((2 * (C * C)) + (2 * (D * D))) + ( - (E * E))) by Lm88A, B2, B3;

          ((2 * x) - ((z . n) + (z . m))) = ((2 * x) + (( - 1) * ((z . n) + (z . m)))) by RLVECT_1: 16

          .= ((2 * x) + ((2 * (1 / 2)) * ( - ((z . n) + (z . m))))) by RLVECT_1: 24

          .= ((2 * x) + (2 * ((1 / 2) * ( - ((z . n) + (z . m)))))) by RLVECT_1:def 7

          .= (2 * (x + ((1 / 2) * ( - ((z . n) + (z . m)))))) by RLVECT_1:def 5

          .= (2 * (x - ((1 / 2) * ((z . n) + (z . m))))) by RLVECT_1: 25;

          

          then

           B7: ||.((2 * x) - ((z . n) + (z . m))).|| = ( |.2.| * ||.(x - ((1 / 2) * ((z . n) + (z . m)))).||) by BHSP_1: 27

          .= (2 * ||.(x - ((1 / 2) * ((z . n) + (z . m)))).||) by ABSVALUE:def 1;

          reconsider znm = ((z . n) + (z . m)) as Point of X;

          reconsider p0 = ||.(x - ((1 / 2) * ((z . n) + (z . m)))).|| as Real;

          (z . n) in M & (z . m) in M by A8;

          then znm in M by RUSUB_1: 14;

          then ((1 / 2) * znm) in M by RUSUB_1: 15;

          then p0 in Y by A3;

          then d <= p0 by A3, A4, SEQ_4:def 2;

          then (2 * d) <= ||.((2 * x) - ((z . n) + (z . m))).|| by B7, XREAL_1: 64;

          then ((2 * d) * (2 * d)) <= ( ||.((2 * x) - ((z . n) + (z . m))).|| * ||.((2 * x) - ((z . n) + (z . m))).||) by A3, XREAL_1: 66;

          then ( - (E * E)) <= ( - (4 * (d * d))) by XREAL_1: 24;

          then

           B81: (F * F) <= (((2 * (C * C)) + (2 * (D * D))) + ( - (4 * (d * d)))) by B6, XREAL_1: 6;

          

           E2: (SA . n) = (2 * (S1 . n)) by SEQ_1: 9

          .= (2 * ((S . n) * (S . n))) by SEQ_1: 8;

          

           E3: (SB . m) = (2 * (S2 . m)) by SEQ_1: 9

          .= (2 * ((S . m) * (S . m))) by SEQ_1: 8;

          

           B91: C = (S . n) & D = (S . m) by A8;

          (((SA . n) + (SB . m)) - (4 * (d * d))) <= |.(((SA . n) + (SB . m)) - (4 * (d * d))).| by ABSVALUE: 4;

          then (F * F) <= |.(((SA . n) + (SB . m)) - (4 * (d * d))).| by B91, B81, E2, E3, XXREAL_0: 2;

          then (F * F) < (p * p) by B0, XXREAL_0: 2;

          then (F ^2 ) < (p * p) by SQUARE_1:def 1;

          then

           B10: (F ^2 ) < (p ^2 ) by SQUARE_1:def 1;

           0 <= (F * F) by XREAL_1: 63;

          then 0 <= (F ^2 ) by SQUARE_1:def 1;

          then

           B11: ( sqrt (F ^2 )) < ( sqrt (p ^2 )) by B10, SQUARE_1: 27;

          

           B12: F < ( sqrt (p ^2 )) by B11, SQUARE_1: 22, BHSP_1: 28;

           ||.((z . n) - (z . m)).|| = ||.( - ((z . m) - (z . n))).|| by RLVECT_1: 33

          .= F by BHSP_1: 31;

          hence thesis by B12, SQUARE_1: 22, AS1;

        end;

        take k;

        thus thesis by D2;

      end;

      then

       A13: z is convergent by BHSP_3:def 4, BHSP_3: 2;

      then

      consider x0 be Point of X such that

       A14: for r be Real st r > 0 holds ex m be Nat st for n be Nat st n >= m holds ||.((z . n) - x0).|| < r by BHSP_2: 9;

      ( lim z) = x0 by A13, A14, BHSP_2: 19;

      

      then

       A16: ( lim ||.(z - x).||) = ||.(x0 - x).|| by A13, BHSP_2: 34

      .= ||.( - (x0 - x)).|| by BHSP_1: 31

      .= ||.(x - x0).|| by RLVECT_1: 33;

      for y be object st y in ( rng z) holds y in N

      proof

        let y be object;

        assume y in ( rng z);

        then ex n be object st n in NAT & (z . n) = y by FUNCT_2: 11;

        then y in M by A8;

        hence thesis by A1;

      end;

      then ( rng z) c= N;

      then

       BX: ( lim z) in N by A1, A13, LM1;

      ex k0 be Nat st for n be Nat st k0 <= n holds (S . n) = ( ||.(z - x).|| . n)

      proof

        set k0 = the Nat;

        

         B1: for n be Nat st k0 <= n holds (S . n) = ( ||.(z - x).|| . n)

        proof

          let n be Nat;

          assume k0 <= n;

          

          thus (S . n) = ||.(x - (z . n)).|| by A8

          .= ||.( - ((z . n) - x)).|| by RLVECT_1: 33

          .= ||.((z . n) + ( - x)).|| by BHSP_1: 31

          .= ||.((z + ( - x)) . n).|| by BHSP_1:def 6

          .= ||.((z - x) . n).|| by BHSP_1: 56

          .= ( ||.(z - x).|| . n) by BHSP_2:def 3;

        end;

        take k0;

        thus thesis by B1;

      end;

      then

       BY: ( lim S) = ( lim ||.(z - x).||) by A5, SEQ_4: 19;

      take x0;

      thus thesis by BX, A1, A13, A14, BHSP_2: 19, BY, SEQ_2:def 7, B5, A16, A5;

    end;

    theorem :: DUALSP04:32

    

     Lm87A: for X be RealHilbertSpace, M be Subspace of X, x,x0 be Point of X, d be Real st x0 in M & (ex Y be non empty Subset of REAL st Y = { ||.(x - y).|| where y be Point of X : y in M } & d = ( lower_bound Y) >= 0 ) holds d = ||.(x - x0).|| iff for w be Point of X st w in M holds (w,(x - x0)) are_orthogonal

    proof

      let X be RealHilbertSpace, M be Subspace of X, x,x0 be Point of X, d be Real;

      assume that

       A2: x0 in M and

       A3: ex Y be non empty Subset of REAL st Y = { ||.(x - y).|| where y be Point of X : y in M } & d = ( lower_bound Y) >= 0 ;

      consider Y be non empty Subset of REAL such that

       A4: Y = { ||.(x - y).|| where y be Point of X : y in M } & d = ( lower_bound Y) >= 0 by A3;

      reconsider r0 = 0 as Real;

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

      proof

        let r be ExtReal;

        assume r in Y;

        then ex y be Point of X st r = ||.(x - y).|| & y in M by A4;

        hence r0 <= r by BHSP_1: 28;

      end;

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

      then

       A51: Y is bounded_below;

      

       A6: for y0 be Point of X st y0 in M holds d <= ||.(x - y0).||

      proof

        let y0 be Point of X;

        assume y0 in M;

        then ||.(x - y0).|| in Y by A4;

        hence thesis by A51, A4, SEQ_4:def 2;

      end;

      hereby

        assume

         AS1: d = ||.(x - x0).||;

        assume not (for w be Point of X st w in M holds (w,(x - x0)) are_orthogonal );

        then

        consider w be Point of X such that

         B1: w in M & (w .|. (x - x0)) <> 0 ;

        set e = (w .|. (x - x0));

        set r = (e / ( ||.w.|| ^2 ));

        set s = ( ||.w.|| ^2 );

        reconsider w0 = (x0 + (r * w)) as Point of X;

        

         B21: (r * w) in M by B1, RUSUB_1: 15;

        per cases ;

          suppose

           C11: s = 0 ;

           ||.w.|| = 0 by C11, SQUARE_1: 17, SQUARE_1: 22, BHSP_1: 28;

          then w = ( 0. X) by BHSP_1: 26;

          hence contradiction by B1, BHSP_1: 14;

        end;

          suppose

           CS2: s <> 0 ;

          

           C2: ( ||.(x - w0).|| ^2 ) = ( ||.((x - x0) - (r * w)).|| ^2 ) by RLVECT_1: 27

          .= ((( ||.(x - x0).|| ^2 ) - (2 * ((x - x0) .|. (r * w)))) + ( ||.(r * w).|| ^2 )) by RUSUB_5: 29;

          

           C3: ((x - x0) .|. (r * w)) = ((e / s) * e) by BHSP_1: 3

          .= ((e * e) / s) by XCMPLX_1: 74

          .= ((e ^2 ) / s) by SQUARE_1:def 1;

          

           C4: ( ||.(r * w).|| ^2 ) = (( |.r.| * ||.w.||) ^2 ) by BHSP_1: 27

          .= (( |.r.| ^2 ) * s) by SQUARE_1: 9

          .= (((e / s) ^2 ) * s) by COMPLEX1: 75

          .= (((e * (1 / s)) ^2 ) * s) by XCMPLX_1: 99

          .= (((e ^2 ) * ((1 / s) ^2 )) * s) by SQUARE_1: 9

          .= ((e ^2 ) * (((1 / s) ^2 ) * s))

          .= ((e ^2 ) * (((1 / s) * (1 / s)) * s)) by SQUARE_1:def 1

          .= ((e ^2 ) * ((1 / s) * ((1 / s) * s)))

          .= ((e ^2 ) * ((1 / s) * 1)) by CS2, XCMPLX_1: 106

          .= ((e ^2 ) / s) by XCMPLX_1: 99;

          

           C5: ( ||.(x - w0).|| ^2 ) = (( ||.(x - x0).|| ^2 ) - ((e ^2 ) / s)) by C3, C4, C2;

          

           C6: 0 < (e ^2 ) by B1, SQUARE_1: 12;

           0 <= ||.w.|| by BHSP_1: 28;

          then 0 <= ( ||.w.|| * ||.w.||);

          then 0 < s by CS2, SQUARE_1:def 1;

          then

           C7: ( ||.(x - w0).|| ^2 ) < ( ||.(x - x0).|| ^2 ) by C5, XREAL_1: 44, C6;

           0 <= ( ||.(x - w0).|| * ||.(x - w0).||) by XREAL_1: 63;

          then 0 <= ( ||.(x - w0).|| ^2 ) by SQUARE_1:def 1;

          then ( sqrt ( ||.(x - w0).|| ^2 )) < ( sqrt ( ||.(x - x0).|| ^2 )) by C7, SQUARE_1: 27;

          then

           C91: ||.(x - w0).|| < ( sqrt ( ||.(x - x0).|| ^2 )) by BHSP_1: 28, SQUARE_1: 22;

          d <= ||.(x - w0).|| by A6, B21, A2, RUSUB_1: 14;

          hence contradiction by C91, AS1, BHSP_1: 28, SQUARE_1: 22;

        end;

      end;

      assume

       AS2: for w be Point of X st w in M holds (w,(x - x0)) are_orthogonal ;

      

       B1: for y be Point of X st y in M holds ||.(x - x0).|| <= ||.(x - y).||

      proof

        let y be Point of X;

        assume y in M;

        then

         C1: ((x0 - y),(x - x0)) are_orthogonal by AS2, A2, RUSUB_1: 17;

        (x - y) = ((x - y) + ( 0. X))

        .= ((x + ( - y)) + (( - x0) + x0)) by RLVECT_1: 5

        .= (((x + ( - y)) + ( - x0)) + x0) by RLVECT_1:def 3

        .= (((x + ( - x0)) + ( - y)) + x0) by RLVECT_1:def 3

        .= ((x - x0) + (x0 - y)) by RLVECT_1:def 3;

        then ( ||.(x - y).|| ^2 ) = (( ||.(x - x0).|| ^2 ) + ( ||.(x0 - y).|| ^2 )) by C1, RUSUB_5: 30;

        then

         C2: (( ||.(x - y).|| ^2 ) - ( ||.(x0 - y).|| ^2 )) = ( ||.(x - x0).|| ^2 );

         0 <= ( ||.(x0 - y).|| * ||.(x0 - y).||) by XREAL_1: 63;

        then

         C31: 0 <= ( ||.(x0 - y).|| ^2 ) by SQUARE_1:def 1;

         0 <= ( ||.(x - x0).|| * ||.(x - x0).||) by XREAL_1: 63;

        then 0 <= ( ||.(x - x0).|| ^2 ) by SQUARE_1:def 1;

        then ( sqrt ( ||.(x - x0).|| ^2 )) <= ( sqrt ( ||.(x - y).|| ^2 )) by C31, C2, XREAL_1: 43, SQUARE_1: 26;

        then ||.(x - x0).|| <= ( sqrt ( ||.(x - y).|| ^2 )) by BHSP_1: 28, SQUARE_1: 22;

        hence ||.(x - x0).|| <= ||.(x - y).|| by BHSP_1: 28, SQUARE_1: 22;

      end;

      for s be Real st s in Y holds ||.(x - x0).|| <= s

      proof

        let s be Real;

        assume s in Y;

        then

        consider y0 be Point of X such that

         C1: s = ||.(x - y0).|| & y0 in M by A4;

        thus ||.(x - x0).|| <= s by B1, C1;

      end;

      then

       B2: ||.(x - x0).|| <= d by A4, SEQ_4: 43;

      d <= ||.(x - x0).|| by A2, A6;

      hence d = ||.(x - x0).|| by B2, XXREAL_0: 1;

    end;

    theorem :: DUALSP04:33

    

     Th87A: for X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X st N = the carrier of M & N is closed holds ex y,z be Point of X st y in M & z in ( Ort_Comp M) & x = (y + z)

    proof

      let X be RealHilbertSpace, M be Subspace of X, N be Subset of X, x be Point of X;

      assume

       AS: N = the carrier of M & N is closed;

      set Y = { ||.(x - y).|| where y be Point of X : y in M };

      Y c= REAL

      proof

        let z be object;

        assume z in Y;

        then

        consider y be Point of X such that

         B1: z = ||.(x - y).|| & y in M;

        thus z in REAL by B1, XREAL_0:def 1;

      end;

      then

      reconsider Y as Subset of REAL ;

      ( 0. X) in M by RUSUB_1: 11;

      then ||.(x - ( 0. X)).|| in Y;

      then

      reconsider Y as non empty Subset of REAL ;

      set d = ( lower_bound Y);

      

       A11: for r be Real st r in Y holds 0 <= r

      proof

        let r be Real;

        assume r in Y;

        then

        consider y be Point of X such that

         B2: r = ||.(x - y).|| & y in M;

        thus 0 <= r by B2, BHSP_1: 28;

      end;

      then

       A1: 0 <= d by SEQ_4: 43;

      consider x0 be Point of X such that

       A2: d = ||.(x - x0).|| & x0 in M by AS, Lm88, A11, SEQ_4: 43;

      reconsider y = x0 as Point of X;

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

      for w be Point of X st w in M holds (w,(x - x0)) are_orthogonal by A1, A2, Lm87A;

      then

       B21: (x - x0) in { v where v be VECTOR of X : for w be Point of X st w in M holds (w,v) are_orthogonal };

      

       B3: (y + z) = ((x0 + ( - x0)) + x) by RLVECT_1:def 3

      .= (x + ( 0. X)) by RLVECT_1: 5

      .= x;

      take y, z;

      thus thesis by A2, B21, RUSUB_5:def 3, B3;

    end;

    theorem :: DUALSP04:34

    for X be RealUnitarySpace, M be Subspace of X, x be Point of X, y1,y2,z1,z2 be Point of X st y1 in M & y2 in M & z1 in ( Ort_Comp M) & z2 in ( Ort_Comp M) & x = (y1 + z1) & x = (y2 + z2) holds y1 = y2 & z1 = z2

    proof

      let X be RealUnitarySpace, M be Subspace of X, x be Point of X;

      let y1,y2,z1,z2 be Point of X;

      assume that

       A1: y1 in M & y2 in M & z1 in ( Ort_Comp M) & z2 in ( Ort_Comp M) and

       A2: x = (y1 + z1) & x = (y2 + z2);

      (y1 + (z1 + ( - y2))) = ((y2 + z2) + ( - y2)) by RLVECT_1:def 3, A2;

      then (y1 + (( - y2) + z1)) = (y2 + (( - y2) + z2)) by RLVECT_1:def 3;

      then ((y1 + ( - y2)) + z1) = (y2 + (( - y2) + z2)) by RLVECT_1:def 3;

      then ((y1 - y2) + z1) = ((y2 + ( - y2)) + z2) by RLVECT_1:def 3;

      then ((y1 - y2) + z1) = (z2 + ( 0. X)) by RLVECT_1:def 10;

      then ((y1 - y2) + (z1 + ( - z1))) = (z2 + ( - z1)) by RLVECT_1:def 3;

      then

       A31: ((y1 - y2) + ( 0. X)) = (z2 + ( - z1)) by RLVECT_1:def 10;

      

       A4: (y1 - y2) in M & (z2 - z1) in ( Ort_Comp M) by A1, RUSUB_1: 17;

      then (y1 - y2) in (the carrier of M /\ the carrier of ( Ort_Comp M)) by XBOOLE_0:def 4, A31;

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

      hence y1 = y2 by RLVECT_1: 21;

      (z2 - z1) in (the carrier of M /\ the carrier of ( Ort_Comp M)) by A4, A31, XBOOLE_0:def 4;

      then (z2 - z1) = ( 0. X) by Lm814;

      hence z1 = z2 by RLVECT_1: 21;

    end;

    begin

    theorem :: DUALSP04:35

    for X be RealUnitarySpace, f be linear-Functional of X, y be Point of X st for x be Point of X holds (f . x) = (x .|. y) holds f is Lipschitzian

    proof

      let X be RealUnitarySpace, f be linear-Functional of X, y be Point of X;

      assume

       AS: for x be Point of X holds (f . x) = (x .|. y);

      reconsider K = ( ||.y.|| + 1) as Real;

      

       A11: 0 <= ||.y.|| by BHSP_1: 28;

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

      proof

        let x be Point of X;

        

         B1: |.(x .|. y).| <= ( ||.x.|| * ||.y.||) by BHSP_1: 29;

        

         B2: ||.y.|| < ( ||.y.|| + 1) by XREAL_1: 145;

         0 <= ||.x.|| by BHSP_1: 28;

        then ( ||.y.|| * ||.x.||) <= (( ||.y.|| + 1) * ||.x.||) by B2, XREAL_1: 64;

        then |.(x .|. y).| <= (( ||.y.|| + 1) * ||.x.||) by B1, XXREAL_0: 2;

        hence thesis by AS;

      end;

      hence thesis by A11, BHSP_6:def 4;

    end;

    

     KERX1: for X be RealUnitarySpace, f be Function of X, REAL st f is homogeneous holds (f " { 0 }) is non empty

    proof

      let X be RealUnitarySpace, f be Function of X, REAL ;

      assume

       A1: f is homogeneous;

      (f . ( 0. X)) = (f . ( 0 * ( 0. X)))

      .= ( 0 * (f . ( 0. X))) by A1, HAHNBAN:def 3

      .= 0 ;

      then (f . ( 0. X)) in { 0 } by TARSKI:def 1;

      hence thesis by FUNCT_2: 38;

    end;

    registration

      let X be RealUnitarySpace, f be linear-Functional of X;

      cluster (f " { 0 }) -> non empty;

      correctness by KERX1;

    end

    theorem :: DUALSP04:36

    

     KLXY1: for X be RealUnitarySpace, f be Function of X, REAL st f is additive homogeneous holds (f " { 0 }) is linearly-closed

    proof

      let X be RealUnitarySpace, f be Function of X, REAL ;

      assume

       A1: f is additive homogeneous;

      set X1 = (f " { 0 });

      

       A2: for v,u be Point of X st v in X1 & u in X1 holds (v + u) in X1

      proof

        let v,u be Point of X;

        assume

         AS1: v in X1 & u in X1;

        then v in the carrier of X & (f . v) in { 0 } by FUNCT_2: 38;

        then

         A3: (f . v) = 0 by TARSKI:def 1;

        

         A4: u in the carrier of X & (f . u) in { 0 } by AS1, FUNCT_2: 38;

        (f . (v + u)) = ((f . v) + (f . u)) by A1, HAHNBAN:def 2

        .= ( 0 + 0 ) by A3, A4, TARSKI:def 1;

        then (f . (v + u)) in { 0 } by TARSKI:def 1;

        hence thesis by FUNCT_2: 38;

      end;

      for r be Real, v be Point of X st v in X1 holds (r * v) in X1

      proof

        let r be Real, v be Point of X;

        assume v in X1;

        then

         A5: v in the carrier of X & (f . v) in { 0 } by FUNCT_2: 38;

        (f . (r * v)) = (r * (f . v)) by A1, HAHNBAN:def 3

        .= (r * 0 ) by A5, TARSKI:def 1;

        then (f . (r * v)) in { 0 } by TARSKI:def 1;

        hence thesis by FUNCT_2: 38;

      end;

      hence thesis by A2;

    end;

    definition

      let X be RealUnitarySpace, f be linear-Functional of X;

      :: DUALSP04:def13

      func UKer (f) -> strict Subspace of X means

      : defuker: the carrier of it = (f " { 0 });

      existence by KLXY1, RUSUB_1: 29;

      uniqueness by RUSUB_1: 24;

    end

    theorem :: DUALSP04:37

    

     Lm89A: for X be RealUnitarySpace, f be linear-Functional of X st f is Lipschitzian holds (f " { 0 }) is closed

    proof

      let X be RealUnitarySpace, f be linear-Functional of X;

      assume

       AS: f is Lipschitzian;

      set Y = (f " { 0 });

      for s be sequence of X st ( rng s) c= Y & s is convergent holds ( lim s) in Y

      proof

        let s be sequence of X;

        assume

         B0: ( rng s) c= Y & s is convergent;

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

        

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

        consider K be Real such that

         B3: 0 < K & for x be Point of X holds |.(f . x).| <= (K * ||.x.||) by AS, BHSP_6:def 4;

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

        proof

          let x1,x2 be Point of X;

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

          

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

          thus thesis by C1, B3;

        end;

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

        then

         B41: f is_continuous_on the carrier of X by LM5;

        

         B5: ( rng s) c= the carrier of X;

        

         B71: f is_continuous_in x0 by B41;

        

         B91: (f /* s) = (f * s) by B1, B5, FUNCT_2:def 11;

        ex k be Nat st for n be Nat st k <= n holds ((f * s) . n) = (( seq_const 0 ) . n)

        proof

          set k = the Nat;

          

           C0: for n be Nat st k <= n holds ((f * s) . n) = (( seq_const 0 ) . n)

          proof

            let n be Nat;

            assume k <= n;

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

            then

             D2: (s . n) in X & (f . (s . n)) in { 0 } by FUNCT_2: 38, B0;

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

            then ((f * s) . n) in { 0 } by ORDINAL1:def 12, D2, FUNCT_1: 13;

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

            hence ((f * s) . n) = (( seq_const 0 ) . n) by SEQ_1: 57;

          end;

          take k;

          thus thesis by C0;

        end;

        

        then ( lim (f * s)) = ( lim ( seq_const 0 )) by SEQ_4: 19

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

        .= 0 ;

        then (f . x0) = 0 by B71, B0, B1, B91;

        then x0 in X & (f . x0) in { 0 } by TARSKI:def 1;

        hence ( lim s) in Y by FUNCT_2: 38;

      end;

      hence (f " { 0 }) is closed by LM1;

    end;

    theorem :: DUALSP04:38

    

     Lm89B: for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V st v <> ( 0. V) holds v in ( Ort_Comp W) implies not v in W

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      assume

       A1: v <> ( 0. V);

      v in ( Ort_Comp W) implies not v in W

      proof

        assume

         A2: v in ( Ort_Comp W);

        assume

         A3: v in W;

        v in { v1 where v1 be VECTOR of V : for w be VECTOR of V st w in W holds (w,v1) are_orthogonal } by A2, RUSUB_5:def 3;

        then ex v1 be VECTOR of V st v = v1 & for w be VECTOR of V st w in W holds (w,v1) are_orthogonal ;

        then (v,v) are_orthogonal by A3;

        hence contradiction by A1, BHSP_1:def 2;

      end;

      hence thesis;

    end;

    theorem :: DUALSP04:39

    

     Th89A: for X be RealHilbertSpace, f be linear-Functional of X st f is Lipschitzian holds ex y be Point of X st for x be Point of X holds (f . x) = (x .|. y)

    proof

      let X be RealHilbertSpace, f be linear-Functional of X;

      assume

       AS: f is Lipschitzian;

      set M = ( UKer f);

      

       A1: the carrier of M = (f " { 0 }) by defuker;

      per cases ;

        suppose

         AS1: the carrier of X = the carrier of M;

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

        

         B1: for x be Point of X holds (f . x) = (x .|. y)

        proof

          let x be Point of X;

          

           C11: x in X & (f . x) in { 0 } by FUNCT_2: 38, AS1, A1;

          (x .|. y) = 0 by BHSP_1: 15;

          hence thesis by C11, TARSKI:def 1;

        end;

        take y;

        thus thesis by B1;

      end;

        suppose the carrier of X <> the carrier of M;

        then not the carrier of X c= the carrier of M by RUSUB_1:def 1;

        then

        consider z be object such that

         B1: z in the carrier of X & not z in the carrier of M;

        reconsider y = z as Point of X by B1;

        reconsider N = the carrier of M as non empty Subset of X by A1;

        consider y1,z1 be Point of X such that

         C0: y1 in M & z1 in ( Ort_Comp M) & y = (y1 + z1) by Th87A, A1, AS, Lm89A;

        

         C1: z1 <> ( 0. X) by C0, B1;

        then ||.z1.|| <> 0 by BHSP_1: 26;

        then

         C2: ( ||.z1.|| ^2 ) > 0 by SQUARE_1: 12;

         not z1 in M by C0, C1, Lm89B;

        then not z1 in (f " { 0 }) by defuker;

        then not (f . z1) in { 0 } by FUNCT_2: 38;

        then

         C3: (f . z1) <> 0 by TARSKI:def 1;

        set r = ((f . z1) / ( ||.z1.|| ^2 ));

        reconsider y = (r * z1) as Point of X;

        

         C4: y in ( Ort_Comp M) by C0, RUSUB_1: 15;

        

         C5: for x be Point of X holds (f . x) = (x .|. y)

        proof

          let x be Point of X;

          set s = ((f . x) / (f . z1));

          reconsider y0 = (x - (s * z1)) as Point of X;

          

           D1: ( - (s * z1)) = (( - 1) * (s * z1)) by RLVECT_1: 16

          .= ((( - 1) * s) * z1) by RLVECT_1:def 7;

          (f . y0) = ((f . x) + (f . ((( - 1) * s) * z1))) by D1, HAHNBAN:def 2

          .= ((f . x) + ((( - 1) * s) * (f . z1))) by HAHNBAN:def 3

          .= ((f . x) - (((f . x) / (f . z1)) * (f . z1)))

          .= ((f . x) - (f . x)) by C3, XCMPLX_1: 87

          .= 0 ;

          then y0 in X & (f . y0) in { 0 } by TARSKI:def 1;

          then y0 in (f " { 0 }) by FUNCT_2: 38;

          then

           D2: y0 in M by defuker;

          y in { v where v be VECTOR of X : for w be VECTOR of X st w in M holds (w,v) are_orthogonal } by RUSUB_5:def 3, C4;

          then

          consider v be VECTOR of X such that

           D3: y = v & for w be VECTOR of X st w in M holds (w,v) are_orthogonal ;

          

           D41: (y0,y) are_orthogonal by D2, D3;

          

           D6: ((x - (s * z1)) .|. (r * z1)) = ((x .|. (r * z1)) - ((s * z1) .|. (r * z1))) by BHSP_1: 11

          .= ((r * (x .|. z1)) - ((s * z1) .|. (r * z1))) by BHSP_1: 3

          .= ((r * (x .|. z1)) - (s * (z1 .|. (r * z1)))) by BHSP_1:def 2;

          

           D7: (s * r) = ((f . x) / ( ||.z1.|| ^2 )) by C3, XCMPLX_1: 98;

          

           D8: 0 <= (z1 .|. z1) by BHSP_1:def 2;

          (z1 .|. (r * z1)) = (r * (z1 .|. z1)) by BHSP_1: 3

          .= (r * ( ||.z1.|| ^2 )) by D8, SQUARE_1:def 2;

          

          then (s * (z1 .|. (r * z1))) = (((f . x) / ( ||.z1.|| ^2 )) * ( ||.z1.|| ^2 )) by D7

          .= (f . x) by C2, XCMPLX_1: 87;

          hence (f . x) = (x .|. y) by BHSP_1: 3, D6, D41;

        end;

        take y;

        thus thesis by C5;

      end;

    end;

    theorem :: DUALSP04:40

    for X be RealUnitarySpace, f be linear-Functional of X holds for y1,y2 be Point of X st for x be Point of X holds (f . x) = (x .|. y1) & (f . x) = (x .|. y2) holds y1 = y2

    proof

      let X be RealUnitarySpace, f be linear-Functional of X;

      let y1,y2 be Point of X;

      assume

       AS: for x be Point of X holds (f . x) = (x .|. y1) & (f . x) = (x .|. y2);

      now

        let x be Point of X;

        (f . x) = (x .|. y1) & (f . x) = (x .|. y2) by AS;

        then ((x .|. y1) - (x .|. y2)) = 0 ;

        hence (x .|. (y1 - y2)) = 0 by BHSP_1: 12;

      end;

      then ((y1 - y2) .|. (y1 - y2)) = 0 ;

      then (y1 - y2) = ( 0. X) by BHSP_1:def 2;

      hence y1 = y2 by RLVECT_1: 21;

    end;

    theorem :: DUALSP04:41

    for X be RealHilbertSpace, f be Point of ( DualSp X), g be Lipschitzian linear-Functional of X st g = f holds ex y be Point of X st (for x be Point of X holds (g . x) = (x .|. y)) & ||.f.|| = ||.y.||

    proof

      let X be RealHilbertSpace, f be Point of ( DualSp X), g be Lipschitzian linear-Functional of X;

      assume

       AS: g = f;

      consider y be Point of X such that

       A1: for x be Point of X holds (g . x) = (x .|. y) by Th89A;

      now

        let s be Real;

        assume s in ( PreNorms g);

        then

        consider t be VECTOR of X such that

         B1: s = |.(g . t).| & ||.t.|| <= 1;

        

         B3: |.(t .|. y).| <= ( ||.t.|| * ||.y.||) by BHSP_1: 29;

         0 <= ||.y.|| by BHSP_1: 28;

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

        then |.(t .|. y).| <= ||.y.|| by B3, XXREAL_0: 2;

        hence s <= ||.y.|| by B1, A1;

      end;

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

      then

       A2: ||.f.|| <= ||.y.|| by AS, Th24;

      

       A31: ||.y.|| <= ||.f.||

      proof

        per cases ;

          suppose ||.y.|| = 0 ;

          hence ||.y.|| <= ||.f.|| by Th27;

        end;

          suppose

           AS2: ||.y.|| <> 0 ;

          

           B1: 0 <= (y .|. y) by BHSP_1:def 2;

          

           B2: (g . y) = (y .|. y) by A1

          .= ( ||.y.|| ^2 ) by B1, SQUARE_1:def 2

          .= ( ||.y.|| * ||.y.||) by SQUARE_1:def 1;

          

           B3: (g . y) <= |.(g . y).| by ABSVALUE: 4;

           |.(g . y).| <= ( ||.f.|| * ||.y.||) by AS, Th26;

          then

           B4: ( ||.y.|| * ||.y.||) <= ( ||.f.|| * ||.y.||) by B2, B3, XXREAL_0: 2;

          

           B51: 0 <= ||.y.|| by BHSP_1: 28;

          (( ||.y.|| * ||.y.||) / ||.y.||) = ||.y.|| & (( ||.f.|| * ||.y.||) / ||.y.||) = ||.f.|| by AS2, XCMPLX_1: 89;

          hence ||.y.|| <= ||.f.|| by B51, B4, XREAL_1: 72;

        end;

      end;

      take y;

      thus thesis by A1, A2, XXREAL_0: 1, A31;

    end;