normsp_2.miz



    begin

    theorem :: NORMSP_2:1

    for X be non empty MetrSpace, Y be SetSequence of X st X is complete & ( union ( rng Y)) = the carrier of X & for n be Nat holds ((Y . n) ` ) in ( Family_open_set X) holds ex n0 be Nat, r be Real, x0 be Point of X st 0 < r & ( Ball (x0,r)) c= (Y . n0)

    proof

      let X be non empty MetrSpace, Y be SetSequence of X;

      assume that

       A1: X is complete and

       A2: ( union ( rng Y)) = the carrier of X and

       A3: for n be Nat holds ((Y . n) ` ) in ( Family_open_set X);

      defpred P[ Nat, Point of X, Real, Point of X, Real] means ( 0 < $3 & $3 < (1 / (2 |^ $1)) & (( Ball ($2,$3)) /\ (Y . $1)) = {} ) implies ( 0 < $5 & $5 < (1 / (2 |^ ($1 + 1))) & ( Ball ($4,$5)) c= ( Ball ($2,($3 / 2))) & (( Ball ($4,$5)) /\ (Y . ($1 + 1))) = {} );

      assume

       A4: not ex n0 be Nat, r be Real, x0 be Point of X st 0 < r & ( Ball (x0,r)) c= (Y . n0);

      now

        set x0 = the Point of X;

        

         A5: (((Y . 0 ) ` ) ` ) = (the carrier of X \ ((Y . 0 ) ` )) & ( Ball (x0,1)) c= the carrier of X;

        assume ((Y . 0 ) ` ) = {} ;

        hence contradiction by A4, A5;

      end;

      then

      consider z0 be object such that

       A6: z0 in ((Y . 0 ) ` ) by XBOOLE_0:def 1;

      reconsider z0 as Element of X by A6;

      ((Y . 0 ) ` ) in ( Family_open_set X) by A3;

      then

      consider t01 be Real such that

       A7: 0 < t01 and

       A8: ( Ball (z0,t01)) c= ((Y . 0 ) ` ) by A6, PCOMPS_1:def 4;

      reconsider t0 = ( min (t01,(1 / 2))) as Element of REAL by XREAL_0:def 1;

      t0 <= (1 / 2) by XXREAL_0: 17;

      then t0 < (1 / 1) by XXREAL_0: 2;

      then

       A9: t0 < (1 / (2 |^ 0 )) by NEWTON: 4;

      ( Ball (z0,t0)) c= ( Ball (z0,t01)) by PCOMPS_1: 1, XXREAL_0: 17;

      then ( Ball (z0,t0)) c= ((Y . 0 ) ` ) by A8;

      then ( Ball (z0,t0)) misses (Y . 0 ) by SUBSET_1: 23;

      then

       A10: (( Ball (z0,t0)) /\ (Y . 0 )) = {} by XBOOLE_0:def 7;

      

       A11: for n be Nat, x be Point of X, r be Real holds ex x1 be Point of X, r1 be Real st 0 < r & r < (1 / (2 |^ n)) & (( Ball (x,r)) /\ (Y . n)) = {} implies 0 < r1 & r1 < (1 / (2 |^ (n + 1))) & ( Ball (x1,r1)) c= ( Ball (x,(r / 2))) & (( Ball (x1,r1)) /\ (Y . (n + 1))) = {}

      proof

        let n be Nat, x be Point of X, r be Real;

        now

           0 < (2 |^ (n + 2)) by NEWTON: 83;

          then

           A12: 0 < (1 / (2 |^ (n + 2))) by XREAL_1: 139;

           0 < (2 |^ (n + 1)) by NEWTON: 83;

          then

           A13: ((1 / (2 |^ (n + 1))) / 2) < (1 / (2 |^ (n + 1))) by XREAL_1: 139, XREAL_1: 216;

          (2 |^ (n + 2)) = (2 |^ ((n + 1) + 1))

          .= ((2 |^ (n + 1)) * 2) by NEWTON: 6;

          then

           A14: (1 / (2 |^ (n + 2))) = ((1 / (2 |^ (n + 1))) / 2) by XCMPLX_1: 78;

          assume that

           A15: 0 < r and r < (1 / (2 |^ n)) and (( Ball (x,r)) /\ (Y . n)) = {} ;

           not ( Ball (x,(r / 2))) c= (Y . (n + 1)) by A4, A15, XREAL_1: 215;

          then ( Ball (x,(r / 2))) meets ((Y . (n + 1)) ` ) by SUBSET_1: 24;

          then

          consider z0 be object such that

           A16: z0 in (( Ball (x,(r / 2))) /\ ((Y . (n + 1)) ` )) by XBOOLE_0: 4;

          reconsider x1 = z0 as Point of X by A16;

          

           A17: ((Y . (n + 1)) ` ) in ( Family_open_set X) by A3;

          ( Ball (x,(r / 2))) in ( Family_open_set X) & ((Y . (n + 1)) ` ) in ( Family_open_set X) by A3, PCOMPS_1: 29;

          then (( Ball (x,(r / 2))) /\ ((Y . (n + 1)) ` )) in ( Family_open_set X) by PCOMPS_1: 31;

          then

          consider t02 be Real such that

           A18: 0 < t02 and

           A19: ( Ball (x1,t02)) c= (( Ball (x,(r / 2))) /\ ((Y . (n + 1)) ` )) by A16, PCOMPS_1:def 4;

          

           A20: ( Ball (x1,t02)) c= ( Ball (x,(r / 2))) by A19, XBOOLE_1: 18;

          x1 in ((Y . (n + 1)) ` ) by A16, XBOOLE_0:def 4;

          then

          consider t01 be Real such that

           A21: 0 < t01 and

           A22: ( Ball (x1,t01)) c= ((Y . (n + 1)) ` ) by A17, PCOMPS_1:def 4;

          reconsider r1 = ( min (( min (t01,t02)),(1 / (2 |^ (n + 2))))) as Real;

          

           A23: r1 <= ( min (t01,t02)) by XXREAL_0: 17;

          ( min (t01,t02)) <= t02 by XXREAL_0: 17;

          then

           A24: ( Ball (x1,r1)) c= ( Ball (x1,t02)) by A23, PCOMPS_1: 1, XXREAL_0: 2;

          ( min (t01,t02)) <= t01 by XXREAL_0: 17;

          then ( Ball (x1,r1)) c= ( Ball (x1,t01)) by A23, PCOMPS_1: 1, XXREAL_0: 2;

          then ( Ball (x1,r1)) c= ((Y . (n + 1)) ` ) by A22;

          then

           A25: ( Ball (x1,r1)) misses (Y . (n + 1)) by SUBSET_1: 23;

          take x1, r1;

          

           A26: r1 <= (1 / (2 |^ (n + 2))) by XXREAL_0: 17;

           0 < ( min (t01,t02)) by A21, A18, XXREAL_0: 15;

          hence P[n, x, r, x1, r1] by A20, A14, A12, A13, A24, A25, A26, XBOOLE_0:def 7, XBOOLE_1: 1, XXREAL_0: 2, XXREAL_0: 15;

        end;

        hence thesis;

      end;

      ex x0 be sequence of X, r0 be Real_Sequence st (x0 . 0 ) = z0 & (r0 . 0 ) = t0 & for n be Nat holds ( 0 < (r0 . n) & (r0 . n) < (1 / (2 |^ n)) & (( Ball ((x0 . n),(r0 . n))) /\ (Y . n)) = {} implies 0 < (r0 . (n + 1)) & (r0 . (n + 1)) < (1 / (2 |^ (n + 1))) & ( Ball ((x0 . (n + 1)),(r0 . (n + 1)))) c= ( Ball ((x0 . n),((r0 . n) / 2))) & (( Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1))) = {} )

      proof

        defpred P1[ Nat, Element of [:the carrier of X, REAL :], Element of [:the carrier of X, REAL :]] means ( 0 < ($2 `2 ) & ($2 `2 ) < (1 / (2 |^ $1)) & (( Ball (($2 `1 ),($2 `2 ))) /\ (Y . $1)) = {} ) implies ( 0 < ($3 `2 ) & ($3 `2 ) < (1 / (2 |^ ($1 + 1))) & ( Ball (($3 `1 ),($3 `2 ))) c= ( Ball (($2 `1 ),(($2 `2 ) / 2))) & (( Ball (($3 `1 ),($3 `2 ))) /\ (Y . ($1 + 1))) = {} );

        

         A27: for n be Nat holds for u be Element of [:the carrier of X, REAL :] holds ex v be Element of [:the carrier of X, REAL :] st P1[n, u, v]

        proof

          let n be Nat, u be Element of [:the carrier of X, REAL :];

          consider v1 be Element of X, v2 be Real such that

           A28: P[n, (u `1 ), (u `2 ), v1, v2] by A11;

          reconsider v2 as Element of REAL by XREAL_0:def 1;

          take [v1, v2];

          thus thesis by A28;

        end;

        consider f be sequence of [:the carrier of X, REAL :] such that

         A29: (f . 0 ) = [z0, t0] & for n be Nat holds P1[n, (f . n), (f . (n + 1))] from RECDEF_1:sch 2( A27);

        take ( pr1 f), ( pr2 f);

        

        thus (( pr1 f) . 0 ) = ((f . 0 ) `1 ) by FUNCT_2:def 5

        .= z0 by A29;

        

        thus (( pr2 f) . 0 ) = ((f . 0 ) `2 ) by FUNCT_2:def 6

        .= t0 by A29;

        hereby

          let i be Nat;

          

           A30: i in NAT by ORDINAL1:def 12;

          

           A31: ((f . (i + 1)) `1 ) = (( pr1 f) . (i + 1)) & ((f . (i + 1)) `2 ) = (( pr2 f) . (i + 1)) by FUNCT_2:def 5, FUNCT_2:def 6;

          ((f . i) `1 ) = (( pr1 f) . i) & ((f . i) `2 ) = (( pr2 f) . i) by FUNCT_2:def 5, FUNCT_2:def 6, A30;

          hence P[i, (( pr1 f) . i), (( pr2 f) . i), (( pr1 f) . (i + 1)), (( pr2 f) . (i + 1))] by A29, A31;

        end;

      end;

      then

      consider x0 be sequence of X, r0 be Real_Sequence such that

       A32: (x0 . 0 ) = z0 & (r0 . 0 ) = t0 and

       A33: for n be Nat holds ( 0 < (r0 . n) & (r0 . n) < (1 / (2 |^ n)) & (( Ball ((x0 . n),(r0 . n))) /\ (Y . n)) = {} implies 0 < (r0 . (n + 1)) & (r0 . (n + 1)) < (1 / (2 |^ (n + 1))) & ( Ball ((x0 . (n + 1)),(r0 . (n + 1)))) c= ( Ball ((x0 . n),((r0 . n) / 2))) & (( Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1))) = {} );

       0 < (1 / 2);

      then

       A34: 0 < t0 by A7, XXREAL_0: 15;

      

       A35: for n be Nat holds 0 < (r0 . n) & (r0 . n) < (1 / (2 |^ n)) & ( Ball ((x0 . (n + 1)),(r0 . (n + 1)))) c= ( Ball ((x0 . n),((r0 . n) / 2))) & (( Ball ((x0 . n),(r0 . n))) /\ (Y . n)) = {}

      proof

        defpred PN[ Nat] means 0 < (r0 . $1) & (r0 . $1) < (1 / (2 |^ $1)) & ( Ball ((x0 . ($1 + 1)),(r0 . ($1 + 1)))) c= ( Ball ((x0 . $1),((r0 . $1) / 2))) & (( Ball ((x0 . $1),(r0 . $1))) /\ (Y . $1)) = {} ;

         A36:

        now

          let n be Nat;

          assume

           A37: PN[n];

          then

           A38: (( Ball ((x0 . (n + 1)),(r0 . (n + 1)))) /\ (Y . (n + 1))) = {} by A33;

           0 < (r0 . (n + 1)) & (r0 . (n + 1)) < (1 / (2 |^ (n + 1))) by A33, A37;

          hence PN[(n + 1)] by A33, A38;

        end;

        

         A39: PN[ 0 ] by A34, A9, A10, A32, A33;

        thus for n be Nat holds PN[n] from NAT_1:sch 2( A39, A36);

      end;

      

       A40: for m,k be Nat holds ( dist ((x0 . (m + k)),(x0 . m))) <= ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k))))

      proof

        let m be Nat;

        defpred PN[ Nat] means ( dist ((x0 . (m + $1)),(x0 . m))) <= ((1 / (2 |^ m)) * (1 - (1 / (2 |^ $1))));

         A41:

        now

          let k be Nat;

          assume PN[k];

          then

           A42: (( dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ( dist ((x0 . (m + k)),(x0 . m)))) <= (( dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k))))) by XREAL_1: 6;

           0 < (r0 . ((m + k) + 1)) & ( dist ((x0 . ((m + k) + 1)),(x0 . ((m + k) + 1)))) = 0 by A35, METRIC_1: 1;

          then

           A43: (x0 . ((m + k) + 1)) in ( Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1)))) by METRIC_1: 11;

          (r0 . (m + k)) < (1 / (2 |^ (m + k))) by A35;

          then ((r0 . (m + k)) / 2) < ((1 / (2 |^ (m + k))) / 2) by XREAL_1: 74;

          then ((r0 . (m + k)) / 2) < (1 / ((2 |^ (m + k)) * 2)) by XCMPLX_1: 78;

          then

           A44: ((r0 . (m + k)) / 2) < (1 / (2 |^ ((m + k) + 1))) by NEWTON: 6;

          ( Ball ((x0 . ((m + k) + 1)),(r0 . ((m + k) + 1)))) c= ( Ball ((x0 . (m + k)),((r0 . (m + k)) / 2))) by A35;

          then ( dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) < ((r0 . (m + k)) / 2) by A43, METRIC_1: 11;

          then ( dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) <= (1 / (2 |^ ((m + k) + 1))) by A44, XXREAL_0: 2;

          then

           A45: (( dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k))))) <= ((1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k))))) by XREAL_1: 6;

          (2 |^ (m + (k + 1))) = ((2 |^ m) * (2 |^ (k + 1))) by NEWTON: 8;

          

          then (1 / (2 |^ ((m + k) + 1))) = ((1 / (2 |^ m)) / ((2 |^ (k + 1)) / 1)) by XCMPLX_1: 78

          .= ((1 / (2 |^ m)) * (1 / (2 |^ (k + 1)))) by XCMPLX_1: 79;

          

          then

           A46: ((1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k))))) = ((1 / (2 |^ m)) * (1 + ((1 / (2 |^ (k + 1))) - (1 / (2 |^ k)))))

          .= ((1 / (2 |^ m)) * (1 + ((1 / ((2 |^ k) * 2)) - (1 / (2 |^ k))))) by NEWTON: 6

          .= ((1 / (2 |^ m)) * (1 + (((1 / (2 |^ k)) / 2) - (1 / (2 |^ k))))) by XCMPLX_1: 78

          .= ((1 / (2 |^ m)) * (1 - ((1 / (2 |^ k)) / 2)))

          .= ((1 / (2 |^ m)) * (1 - (1 / ((2 |^ k) * 2)))) by XCMPLX_1: 78;

          ( dist ((x0 . ((m + k) + 1)),(x0 . m))) <= (( dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ( dist ((x0 . (m + k)),(x0 . m)))) by METRIC_1: 4;

          then ( dist ((x0 . (m + (k + 1))),(x0 . m))) <= (( dist ((x0 . ((m + k) + 1)),(x0 . (m + k)))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k))))) by A42, XXREAL_0: 2;

          then ( dist ((x0 . (m + (k + 1))),(x0 . m))) <= ((1 / (2 |^ ((m + k) + 1))) + ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k))))) by A45, XXREAL_0: 2;

          hence PN[(k + 1)] by A46, NEWTON: 6;

        end;

        (2 |^ 0 ) = 1 by NEWTON: 4;

        then

         A47: PN[ 0 ] by METRIC_1: 1;

        for k be Nat holds PN[k] from NAT_1:sch 2( A47, A41);

        hence thesis;

      end;

       A48:

      now

        let m be Nat;

        hereby

          let k be Nat;

          

           A49: ( dist ((x0 . (m + k)),(x0 . m))) <= ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) by A40;

           0 < (2 |^ k) by NEWTON: 83;

          then 0 < (1 / (2 |^ k)) by XREAL_1: 139;

          then

           A50: (1 - (1 / (2 |^ k))) < (1 - 0 ) by XREAL_1: 10;

           0 < (2 |^ m) by NEWTON: 83;

          then 0 < (1 / (2 |^ m)) by XREAL_1: 139;

          then ((1 / (2 |^ m)) * (1 - (1 / (2 |^ k)))) < ((1 / (2 |^ m)) * 1) by A50, XREAL_1: 68;

          hence ( dist ((x0 . (m + k)),(x0 . m))) < (1 / (2 |^ m)) by A49, XXREAL_0: 2;

        end;

      end;

      now

        let r be Real;

        assume 0 < r;

        then

        consider p1 be Nat such that

         A51: (1 / (2 |^ p1)) <= r by PREPOWER: 92;

        reconsider p = (p1 + 1) as Nat;

        take p;

        hereby

          let n,m be Nat;

          assume that

           A52: n >= p and

           A53: m >= p;

          consider k1 be Nat such that

           A54: n = (p + k1) by A52, NAT_1: 10;

          reconsider k1 as Nat;

          n = (p + k1) by A54;

          then

           A55: ( dist ((x0 . n),(x0 . p))) < (1 / (2 |^ p)) by A48;

          consider k2 be Nat such that

           A56: m = (p + k2) by A53, NAT_1: 10;

          reconsider k2 as Nat;

          

           A57: (1 / (2 |^ p)) = (1 / ((2 |^ p1) * 2)) by NEWTON: 6

          .= ((1 / (2 |^ p1)) / 2) by XCMPLX_1: 78;

          m = (p + k2) by A56;

          then

           A58: (( dist ((x0 . n),(x0 . p))) + ( dist ((x0 . p),(x0 . m)))) < ((1 / (2 |^ p)) + (1 / (2 |^ p))) by A48, A55, XREAL_1: 8;

          ( dist ((x0 . n),(x0 . m))) <= (( dist ((x0 . n),(x0 . p))) + ( dist ((x0 . p),(x0 . m)))) by METRIC_1: 4;

          then ( dist ((x0 . n),(x0 . m))) < (1 / (2 |^ p1)) by A58, A57, XXREAL_0: 2;

          hence ( dist ((x0 . n),(x0 . m))) < r by A51, XXREAL_0: 2;

        end;

      end;

      then x0 is Cauchy by TBSP_1:def 4;

      then

       A59: x0 is convergent by A1, TBSP_1:def 5;

      

       A60: for m,k be Nat holds ( Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k)))) c= ( Ball ((x0 . m),((r0 . m) / 2)))

      proof

        let m be Nat;

        defpred PN[ Nat] means ( Ball ((x0 . ((m + 1) + $1)),(r0 . ((m + 1) + $1)))) c= ( Ball ((x0 . m),((r0 . m) / 2)));

         A61:

        now

          let k be Nat;

          assume

           A62: PN[k];

           0 < (r0 . ((m + 1) + k)) by A35;

          then ((r0 . ((m + 1) + k)) / 2) < (r0 . ((m + 1) + k)) by XREAL_1: 216;

          then

           A63: ( Ball ((x0 . ((m + 1) + k)),((r0 . ((m + 1) + k)) / 2))) c= ( Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k)))) by PCOMPS_1: 1;

          ( Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1))))) = ( Ball ((x0 . (((m + 1) + k) + 1)),(r0 . (((m + 1) + k) + 1))));

          then ( Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1))))) c= ( Ball ((x0 . ((m + 1) + k)),((r0 . ((m + 1) + k)) / 2))) by A35;

          then ( Ball ((x0 . ((m + 1) + (k + 1))),(r0 . ((m + 1) + (k + 1))))) c= ( Ball ((x0 . ((m + 1) + k)),(r0 . ((m + 1) + k)))) by A63;

          hence PN[(k + 1)] by A62, XBOOLE_1: 1;

        end;

        

         A64: PN[ 0 ] by A35;

        thus for k be Nat holds PN[k] from NAT_1:sch 2( A64, A61);

      end;

       A65:

      now

        let m be Nat;

        set m1 = (m + 1);

         0 < (r0 . m) by A35;

        then 0 < ((r0 . m) / 2) by XREAL_1: 215;

        then

        consider n1 be Nat such that

         A66: for l be Nat st n1 <= l holds ( dist ((x0 . l),( lim x0))) < ((r0 . m) / 2) by A59, TBSP_1:def 3;

        reconsider n = ( max (n1,(m + 1))) as Nat by TARSKI: 1;

        

         A67: ( dist ((x0 . n),( lim x0))) < ((r0 . m) / 2) by A66, XXREAL_0: 25;

        consider k be Nat such that

         A68: n = (m1 + k) by NAT_1: 10, XXREAL_0: 25;

        ( dist ((x0 . n),(x0 . n))) = 0 & 0 < (r0 . n) by A35, METRIC_1: 1;

        then

         A69: (x0 . n) in ( Ball ((x0 . n),(r0 . n))) by METRIC_1: 11;

        reconsider k as Nat;

        n = (m1 + k) by A68;

        then ( Ball ((x0 . n),(r0 . n))) c= ( Ball ((x0 . m),((r0 . m) / 2))) by A60;

        then ( dist ((x0 . n),(x0 . m))) < ((r0 . m) / 2) by A69, METRIC_1: 11;

        then

         A70: (( dist (( lim x0),(x0 . n))) + ( dist ((x0 . n),(x0 . m)))) < (((r0 . m) / 2) + ((r0 . m) / 2)) by A67, XREAL_1: 8;

        ( dist (( lim x0),(x0 . m))) <= (( dist (( lim x0),(x0 . n))) + ( dist ((x0 . n),(x0 . m)))) by METRIC_1: 4;

        then ( dist (( lim x0),(x0 . m))) < (((r0 . m) / 2) + ((r0 . m) / 2)) by A70, XXREAL_0: 2;

        hence ( lim x0) in ( Ball ((x0 . m),(r0 . m))) by METRIC_1: 11;

      end;

       A71:

      now

        let n be Nat;

        thus not ( lim x0) in (Y . n)

        proof

          assume

           A72: ( lim x0) in (Y . n);

          ( lim x0) in ( Ball ((x0 . n),(r0 . n))) by A65;

          then ( lim x0) in (( Ball ((x0 . n),(r0 . n))) /\ (Y . n)) by A72, XBOOLE_0:def 4;

          hence contradiction by A35;

        end;

      end;

       not ( lim x0) in ( union ( rng Y))

      proof

        assume ( lim x0) in ( union ( rng Y));

        then

        consider A be set such that

         A73: ( lim x0) in A and

         A74: A in ( rng Y) by TARSKI:def 4;

        ex k be object st k in ( dom Y) & A = (Y . k) by A74, FUNCT_1:def 3;

        hence contradiction by A71, A73;

      end;

      hence contradiction by A2;

    end;

    begin

    reserve X for RealNormSpace;

    definition

      let X be RealNormSpace;

      :: NORMSP_2:def1

      func distance_by_norm_of X -> Function of [:the carrier of X, the carrier of X:], REAL means

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

      existence

      proof

        set CX = the carrier of X;

        deffunc F( Element of CX, Element of CX) = ( In ( ||.($1 - $2).||, REAL ));

        consider f be Function of [:CX, CX:], REAL such that

         A1: for x be Element of CX holds for y be Element of CX holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take f;

        let x,y be Point of X;

        (f . (x,y)) = F(x,y) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let dist1,dist2 be Function of [:the carrier of X, the carrier of X:], REAL ;

        assume that

         A2: for x,y be Point of X holds (dist1 . (x,y)) = ||.(x - y).|| and

         A3: for x,y be Point of X holds (dist2 . (x,y)) = ||.(x - y).||;

        now

          let x,y be Point of X;

          (dist1 . (x,y)) = ||.(x - y).|| by A2;

          hence (dist1 . (x,y)) = (dist2 . (x,y)) by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    

     Lm1: the distance of MetrStruct (# the carrier of X, ( distance_by_norm_of X) #) is Reflexive

    proof

      now

        let a be Element of X;

        

        thus (( distance_by_norm_of X) . (a,a)) = ||.(a - a).|| by Def1

        .= 0 by NORMSP_1: 6;

      end;

      hence thesis;

    end;

    

     Lm2: the distance of MetrStruct (# the carrier of X, ( distance_by_norm_of X) #) is discerning

    proof

      now

        let a,b be Element of X;

        assume

         A1: (( distance_by_norm_of X) . (a,b)) = 0 ;

        (( distance_by_norm_of X) . (a,b)) = ||.(a - b).|| by Def1;

        hence a = b by A1, NORMSP_1: 6;

      end;

      hence thesis;

    end;

    

     Lm3: the distance of MetrStruct (# the carrier of X, ( distance_by_norm_of X) #) is symmetric

    proof

      now

        let a,b be Element of X;

        

        thus (( distance_by_norm_of X) . (a,b)) = ||.(a - b).|| by Def1

        .= ||.(b - a).|| by NORMSP_1: 7

        .= (( distance_by_norm_of X) . (b,a)) by Def1;

      end;

      hence thesis;

    end;

    

     Lm4: the distance of MetrStruct (# the carrier of X, ( distance_by_norm_of X) #) is triangle

    proof

      now

        let a,b,c be Element of X;

        

         A1: ||.(a - c).|| <= ( ||.(a - b).|| + ||.(b - c).||) by NORMSP_1: 10;

        ( ||.(a - b).|| + ||.(b - c).||) = ( ||.(a - b).|| + (( distance_by_norm_of X) . (b,c))) by Def1

        .= ((( distance_by_norm_of X) . (a,b)) + (( distance_by_norm_of X) . (b,c))) by Def1;

        hence (( distance_by_norm_of X) . (a,c)) <= ((( distance_by_norm_of X) . (a,b)) + (( distance_by_norm_of X) . (b,c))) by A1, Def1;

      end;

      hence thesis;

    end;

    definition

      let X be RealNormSpace;

      :: NORMSP_2:def2

      func MetricSpaceNorm X -> non empty MetrSpace equals MetrStruct (# the carrier of X, ( distance_by_norm_of X) #);

      coherence by Lm1, Lm2, Lm3, Lm4, METRIC_1:def 6, METRIC_1:def 7, METRIC_1:def 8, METRIC_1:def 9;

    end

    theorem :: NORMSP_2:2

    

     Th2: for X be RealNormSpace, z be Element of ( MetricSpaceNorm X), r be Real holds ex x be Point of X st x = z & ( Ball (z,r)) = { y where y be Point of X : ||.(x - y).|| < r }

    proof

      let X be RealNormSpace, z be Element of ( MetricSpaceNorm X), r be Real;

      set M = ( MetricSpaceNorm X);

      reconsider x = z as Point of X;

      

       A1: ( Ball (z,r)) = { q where q be Element of M : ( dist (z,q)) < r } by METRIC_1:def 14;

      now

        let a be object;

        assume a in { y where y be Point of X : ||.(x - y).|| < r };

        then

        consider y be Point of X such that

         A2: a = y & ||.(x - y).|| < r;

        reconsider t = y as Element of M;

         ||.(x - y).|| = ( dist (z,t)) by Def1;

        hence a in { q where q be Element of M : ( dist (z,q)) < r } by A2;

      end;

      then

       A3: { y where y be Point of X : ||.(x - y).|| < r } c= { q where q be Element of M : ( dist (z,q)) < r };

      now

        let a be object;

        assume a in { q where q be Element of M : ( dist (z,q)) < r };

        then

        consider q be Element of M such that

         A4: a = q & ( dist (z,q)) < r;

        reconsider t = q as Point of X;

         ||.(x - t).|| = ( dist (z,q)) by Def1;

        hence a in { y where y be Point of X : ||.(x - y).|| < r } by A4;

      end;

      then { q where q be Element of M : ( dist (z,q)) < r } c= { y where y be Point of X : ||.(x - y).|| < r };

      then { q where q be Element of M : ( dist (z,q)) < r } = { y where y be Point of X : ||.(x - y).|| < r } by A3, XBOOLE_0:def 10;

      hence thesis by A1;

    end;

    theorem :: NORMSP_2:3

    

     Th3: for X be RealNormSpace, z be Element of ( MetricSpaceNorm X), r be Real holds ex x be Point of X st x = z & ( cl_Ball (z,r)) = { y where y be Point of X : ||.(x - y).|| <= r }

    proof

      let X be RealNormSpace, z be Element of ( MetricSpaceNorm X), r be Real;

      reconsider x = z as Point of X;

      set M = ( MetricSpaceNorm X);

      

       A1: ( cl_Ball (z,r)) = { q where q be Element of M : ( dist (z,q)) <= r } by METRIC_1:def 15;

      now

        let a be object;

        assume a in { y where y be Point of X : ||.(x - y).|| <= r };

        then

        consider y be Point of X such that

         A2: a = y & ||.(x - y).|| <= r;

        reconsider t = y as Element of M;

         ||.(x - y).|| = ( dist (z,t)) by Def1;

        hence a in { q where q be Element of M : ( dist (z,q)) <= r } by A2;

      end;

      then

       A3: { y where y be Point of X : ||.(x - y).|| <= r } c= { q where q be Element of M : ( dist (z,q)) <= r };

      now

        let a be object;

        assume a in { q where q be Element of M : ( dist (z,q)) <= r };

        then

        consider q be Element of M such that

         A4: a = q & ( dist (z,q)) <= r;

        reconsider t = q as Point of X;

         ||.(x - t).|| = ( dist (z,q)) by Def1;

        hence a in { y where y be Point of X : ||.(x - y).|| <= r } by A4;

      end;

      then { q where q be Element of M : ( dist (z,q)) <= r } c= { y where y be Point of X : ||.(x - y).|| <= r };

      then { q where q be Element of M : ( dist (z,q)) <= r } = { y where y be Point of X : ||.(x - y).|| <= r } by A3, XBOOLE_0:def 10;

      hence thesis by A1;

    end;

    theorem :: NORMSP_2:4

    

     Th4: for X be RealNormSpace, S be sequence of X, St be sequence of ( MetricSpaceNorm X), x be Point of X, xt be Point of ( MetricSpaceNorm X) st S = St & x = xt holds St is_convergent_in_metrspace_to xt iff for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((S . n) - x).|| < r

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( MetricSpaceNorm X), x be Point of X, xt be Point of ( MetricSpaceNorm X);

      assume

       A1: S = St & x = xt;

       A2:

      now

        assume

         A3: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((S . n) - x).|| < r;

        now

          let r be Real;

          assume r > 0 ;

          then

          consider m be Nat such that

           A4: for n be Nat st m <= n holds ||.((S . n) - x).|| < r by A3;

          take m;

          let n be Nat;

          assume m <= n;

          then ||.((S . n) - x).|| < r by A4;

          hence ( dist ((St . n),xt)) < r by A1, Def1;

        end;

        hence St is_convergent_in_metrspace_to xt by METRIC_6:def 2;

      end;

      now

        assume

         A5: St is_convergent_in_metrspace_to xt;

        let r be Real;

        assume 0 < r;

        then

        consider m be Nat such that

         A6: for n be Nat st m <= n holds ( dist ((St . n),xt)) < r by A5, METRIC_6:def 2;

        take m;

        let n be Nat;

        assume m <= n;

        then ( dist ((St . n),xt)) < r by A6;

        hence ||.((S . n) - x).|| < r by A1, Def1;

      end;

      hence thesis by A2;

    end;

    theorem :: NORMSP_2:5

    

     Th5: for X be RealNormSpace, S be sequence of X, St be sequence of ( MetricSpaceNorm X) st S = St holds St is convergent iff S is convergent

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( MetricSpaceNorm X);

      assume

       A1: S = St;

       A2:

      now

        assume S is convergent;

        then

        consider x be Point of X such that

         A3: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((S . n) - x).|| < r by NORMSP_1:def 6;

        reconsider xt = x as Point of ( MetricSpaceNorm X);

        St is_convergent_in_metrspace_to xt by A1, A3, Th4;

        hence St is convergent by METRIC_6: 9;

      end;

      now

        assume St is convergent;

        then

        consider xt be Point of ( MetricSpaceNorm X) such that

         A4: St is_convergent_in_metrspace_to xt by METRIC_6: 10;

        reconsider x = xt as Point of X;

        for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((S . n) - x).|| < r by A1, A4, Th4;

        hence S is convergent by NORMSP_1:def 6;

      end;

      hence thesis by A2;

    end;

    theorem :: NORMSP_2:6

    

     Th6: for X be RealNormSpace, S be sequence of X, St be sequence of ( MetricSpaceNorm X) st S = St & St is convergent holds ( lim St) = ( lim S)

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( MetricSpaceNorm X);

      assume that

       A1: S = St and

       A2: St is convergent;

      reconsider xt = ( lim S) as Point of ( MetricSpaceNorm X);

      S is convergent by A1, A2, Th5;

      then for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((S . n) - ( lim S)).|| < r by NORMSP_1:def 7;

      then St is_convergent_in_metrspace_to xt by A1, Th4;

      hence thesis by METRIC_6: 11;

    end;

    begin

    definition

      let X be RealNormSpace;

      :: NORMSP_2:def3

      func TopSpaceNorm X -> non empty TopSpace equals ( TopSpaceMetr ( MetricSpaceNorm X));

      coherence ;

    end

    theorem :: NORMSP_2:7

    

     Th7: for X be RealNormSpace, V be Subset of ( TopSpaceNorm X) holds V is open iff for x be Point of X st x in V holds ex r be Real st r > 0 & { y where y be Point of X : ||.(x - y).|| < r } c= V

    proof

      let X be RealNormSpace, V be Subset of ( TopSpaceNorm X);

       A1:

      now

        assume

         A2: for x be Point of X st x in V holds ex r be Real st r > 0 & { y where y be Point of X : ||.(x - y).|| < r } c= V;

        now

          let z be Element of ( MetricSpaceNorm X);

          reconsider x = z as Point of X;

          assume z in V;

          then

          consider r be Real such that

           A3: r > 0 & { y where y be Point of X : ||.(x - y).|| < r } c= V by A2;

          take r;

          ex t be Point of X st t = z & ( Ball (z,r)) = { y where y be Point of X : ||.(t - y).|| < r } by Th2;

          hence r > 0 & ( Ball (z,r)) c= V by A3;

        end;

        hence V in the topology of ( TopSpaceNorm X) by PCOMPS_1:def 4;

        hence V is open;

      end;

      now

        assume

         A4: V is open;

        hereby

          let x be Point of X such that

           A5: x in V;

          reconsider z = x as Element of ( MetricSpaceNorm X);

          V in the topology of ( TopSpaceNorm X) by A4;

          then

          consider r be Real such that

           A6: r > 0 & ( Ball (z,r)) c= V by A5, PCOMPS_1:def 4;

          take r;

          ex t be Point of X st t = z & ( Ball (z,r)) = { y where y be Point of X : ||.(t - y).|| < r } by Th2;

          hence r > 0 & { y where y be Point of X : ||.(x - y).|| < r } c= V by A6;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: NORMSP_2:8

    

     Th8: for X be RealNormSpace, x be Point of X, r be Real holds { y where y be Point of X : ||.(x - y).|| < r } is open Subset of ( TopSpaceNorm X)

    proof

      let X be RealNormSpace, x be Point of X, r be Real;

      reconsider z = x as Element of ( MetricSpaceNorm X);

      (ex t be Point of X st t = x & ( Ball (z,r)) = { y where y be Point of X : ||.(t - y).|| < r }) & ( Ball (z,r)) in ( Family_open_set ( MetricSpaceNorm X)) by Th2, PCOMPS_1: 29;

      hence thesis by PRE_TOPC:def 2;

    end;

    theorem :: NORMSP_2:9

    for X be RealNormSpace, x be Point of X, r be Real holds { y where y be Point of X : ||.(x - y).|| <= r } is closed Subset of ( TopSpaceNorm X)

    proof

      let X be RealNormSpace, x be Point of X, r be Real;

      reconsider z = x as Element of ( MetricSpaceNorm X);

      ex t be Point of X st t = x & ( cl_Ball (z,r)) = { y where y be Point of X : ||.(t - y).|| <= r } by Th3;

      hence thesis by TOPREAL6: 57;

    end;

    ::$Notion-Name

    theorem :: NORMSP_2:10

    for X be Hausdorff non empty TopSpace st X is locally-compact holds X is Baire

    proof

      let X be Hausdorff non empty TopSpace;

      assume X is locally-compact;

      then X is sober locally-compact by YELLOW_8: 22;

      hence thesis by WAYBEL12: 44;

    end;

    theorem :: NORMSP_2:11

    for X be RealNormSpace holds ( TopSpaceNorm X) is sequential;

    registration

      let X be RealNormSpace;

      cluster ( TopSpaceNorm X) -> sequential;

      coherence ;

    end

    theorem :: NORMSP_2:12

    

     Th12: for X be RealNormSpace, S be sequence of X, St be sequence of ( TopSpaceNorm X), x be Point of X, xt be Point of ( TopSpaceNorm X) st S = St & x = xt holds St is_convergent_to xt iff for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((S . n) - x).|| < r

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( TopSpaceNorm X), x be Point of X, xt be Point of ( TopSpaceNorm X);

      assume that

       A1: S = St and

       A2: x = xt;

      reconsider Sm = St as sequence of ( MetricSpaceNorm X);

      reconsider xm = x as Point of ( MetricSpaceNorm X);

      St is_convergent_to xt iff Sm is_convergent_in_metrspace_to xm by A2, FRECHET2: 28;

      hence thesis by A1, Th4;

    end;

    theorem :: NORMSP_2:13

    

     Th13: for X be RealNormSpace, S be sequence of X, St be sequence of ( TopSpaceNorm X) st S = St holds St is convergent iff S is convergent

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( TopSpaceNorm X);

      reconsider Sm = St as sequence of ( MetricSpaceNorm X);

      

       A1: St is convergent iff Sm is convergent by FRECHET2: 29;

      assume S = St;

      hence thesis by A1, Th5;

    end;

    theorem :: NORMSP_2:14

    

     Th14: for X be RealNormSpace, S be sequence of X, St be sequence of ( TopSpaceNorm X) st S = St & St is convergent holds ( Lim St) = {( lim S)} & ( lim St) = ( lim S)

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( TopSpaceNorm X);

      assume that

       A1: S = St and

       A2: St is convergent;

      consider x be Point of ( TopSpaceNorm X) such that

       A3: ( Lim St) = {x} by A2, FRECHET2: 24;

      reconsider Sm = St as sequence of ( MetricSpaceNorm X);

      

       A4: Sm is convergent by A2, FRECHET2: 29;

      

      then

       A5: ( lim St) = ( lim Sm) by FRECHET2: 30

      .= ( lim S) by A1, A4, Th6;

      x in ( Lim St) by A3, TARSKI:def 1;

      then St is_convergent_to x by FRECHET:def 5;

      hence ( Lim St) = {( lim S)} by A5, A3, FRECHET2: 25;

      thus thesis by A5;

    end;

    theorem :: NORMSP_2:15

    

     Th15: for X be RealNormSpace, V be Subset of X, Vt be Subset of ( TopSpaceNorm X) st V = Vt holds V is closed iff Vt is closed

    proof

      let X be RealNormSpace, V be Subset of X, Vt be Subset of ( TopSpaceNorm X);

      assume

       A1: V = Vt;

      hereby

        assume

         A2: V is closed;

        now

          let St be sequence of ( TopSpaceNorm X);

          assume that

           A3: St is convergent and

           A4: ( rng St) c= Vt;

          reconsider S = St as sequence of X;

          S is convergent by A3, Th13;

          then ( lim S) in V by A1, A2, A4, NFCONT_1:def 3;

          then {( lim S)} c= V by ZFMISC_1: 31;

          hence ( Lim St) c= Vt by A1, A3, Th14;

        end;

        hence Vt is closed by FRECHET:def 7;

      end;

      assume

       A5: Vt is closed;

      now

        let S be sequence of X;

        assume that

         A6: ( rng S) c= V and

         A7: S is convergent;

        reconsider St = S as sequence of ( TopSpaceNorm X);

        

         A8: St is convergent by A7, Th13;

        then ( Lim St) c= Vt by A1, A5, A6, FRECHET:def 7;

        then {( lim S)} c= V by A1, A8, Th14;

        hence ( lim S) in V by ZFMISC_1: 31;

      end;

      hence thesis by NFCONT_1:def 3;

    end;

    theorem :: NORMSP_2:16

    

     Th16: for X be RealNormSpace, V be Subset of X, Vt be Subset of ( TopSpaceNorm X) st V = Vt holds V is open iff Vt is open

    proof

      let X be RealNormSpace, V be Subset of X, Vt be Subset of ( TopSpaceNorm X);

      

       A1: V is open iff (V ` ) is closed by NFCONT_1:def 4;

      assume V = Vt;

      then V is open iff (Vt ` ) is closed by A1, Th15;

      hence thesis by TOPS_1: 4;

    end;

    

     Lm5: for X be RealNormSpace, r be Real, x be Point of X holds { y where y be Point of X : ||.(x - y).|| < r } = { y where y be Point of X : ||.(y - x).|| < r }

    proof

      let X be RealNormSpace, r be Real, x be Point of X;

      now

        let s be object;

        assume s in { y where y be Point of X : ||.(y - x).|| < r };

        then

        consider z be Point of X such that

         A1: s = z and

         A2: ||.(z - x).|| < r;

         ||.(x - z).|| < r by A2, NORMSP_1: 7;

        hence s in { y where y be Point of X : ||.(x - y).|| < r } by A1;

      end;

      then

       A3: { y where y be Point of X : ||.(y - x).|| < r } c= { y where y be Point of X : ||.(x - y).|| < r };

      now

        let s be object;

        assume s in { y where y be Point of X : ||.(x - y).|| < r };

        then

        consider z be Point of X such that

         A4: s = z and

         A5: ||.(x - z).|| < r;

         ||.(z - x).|| < r by A5, NORMSP_1: 7;

        hence s in { y where y be Point of X : ||.(y - x).|| < r } by A4;

      end;

      then { y where y be Point of X : ||.(x - y).|| < r } c= { y where y be Point of X : ||.(y - x).|| < r };

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: NORMSP_2:17

    

     Th17: for X be RealNormSpace, U be Subset of X, Ut be Subset of ( TopSpaceNorm X), x be Point of X, xt be Point of ( TopSpaceNorm X) st U = Ut & x = xt holds U is Neighbourhood of x iff Ut is a_neighborhood of xt

    proof

      let X be RealNormSpace, U be Subset of X, Ut be Subset of ( TopSpaceNorm X), x be Point of X, xt be Point of ( TopSpaceNorm X);

      assume that

       A1: U = Ut and

       A2: x = xt;

       A3:

      now

        assume U is Neighbourhood of x;

        then

        consider r be Real such that

         A4: r > 0 and

         A5: { y where y be Point of X : ||.(y - x).|| < r } c= U by NFCONT_1:def 1;

        now

          let s be object;

          assume s in { y where y be Point of X : ||.(y - x).|| < r };

          then ex z be Point of X st s = z & ||.(z - x).|| < r;

          hence s in the carrier of X;

        end;

        then

        reconsider Vt = { y where y be Point of X : ||.(y - x).|| < r } as Subset of ( TopSpaceNorm X) by TARSKI:def 3;

        Vt = { y where y be Point of X : ||.(x - y).|| < r } by Lm5;

        then

         A6: Vt is open by Th8;

         ||.(x - x).|| = 0 by NORMSP_1: 6;

        then xt in Vt by A2, A4;

        hence Ut is a_neighborhood of xt by A1, A5, A6, CONNSP_2: 6;

      end;

      now

        assume Ut is a_neighborhood of xt;

        then

        consider Vt be Subset of ( TopSpaceNorm X) such that

         A7: Vt is open and

         A8: Vt c= Ut and

         A9: xt in Vt by CONNSP_2: 6;

        consider r be Real such that

         A10: r > 0 and

         A11: { y where y be Point of X : ||.(x - y).|| < r } c= Vt by A2, A7, A9, Th7;

        

         A12: { y where y be Point of X : ||.(x - y).|| < r } = { y where y be Point of X : ||.(y - x).|| < r } by Lm5;

        { y where y be Point of X : ||.(x - y).|| < r } c= U by A1, A8, A11;

        hence U is Neighbourhood of x by A10, A12, NFCONT_1:def 1;

      end;

      hence thesis by A3;

    end;

    theorem :: NORMSP_2:18

    

     Th18: for X,Y be RealNormSpace, f be PartFunc of X, Y, ft be Function of ( TopSpaceNorm X), ( TopSpaceNorm Y), x be Point of X, xt be Point of ( TopSpaceNorm X) st f = ft & x = xt holds f is_continuous_in x iff ft is_continuous_at xt

    proof

      let X,Y be RealNormSpace, f be PartFunc of X, Y, ft be Function of ( TopSpaceNorm X), ( TopSpaceNorm Y), x be Point of X, xt be Point of ( TopSpaceNorm X);

      assume that

       A1: f = ft and

       A2: x = xt;

      

       A3: ( dom f) = the carrier of X by A1, FUNCT_2:def 1;

      then

       A4: (ft . xt) = (f /. x) by A1, A2, PARTFUN1:def 6;

      hereby

        assume

         A5: f is_continuous_in x;

        now

          let G be a_neighborhood of (ft . xt);

          reconsider N1 = G as Subset of Y;

          N1 is Neighbourhood of (f /. x) by A4, Th17;

          then

          consider N be Neighbourhood of x such that

           A6: (f .: N) c= N1 by A5, NFCONT_1: 10;

          reconsider H = N as a_neighborhood of xt by A2, Th17;

          take H;

          thus (ft .: H) c= G by A1, A6;

        end;

        hence ft is_continuous_at xt by TMAP_1:def 2;

      end;

      assume

       A7: ft is_continuous_at xt;

      now

        let N1 be Neighbourhood of (f /. x);

        reconsider G = N1 as Subset of Y;

        G is a_neighborhood of (ft . xt) by A4, Th17;

        then

        consider H be a_neighborhood of xt such that

         A8: (ft .: H) c= G by A7, TMAP_1:def 2;

        reconsider N = H as Subset of X;

        reconsider N as Neighbourhood of x by A2, Th17;

        take N;

        thus (f .: N) c= N1 by A1, A8;

      end;

      hence thesis by A3, NFCONT_1: 10;

    end;

    theorem :: NORMSP_2:19

    for X,Y be RealNormSpace, f be PartFunc of X, Y, ft be Function of ( TopSpaceNorm X), ( TopSpaceNorm Y) st f = ft holds f is_continuous_on the carrier of X iff ft is continuous

    proof

      let X,Y be RealNormSpace, f be PartFunc of X, Y, ft be Function of ( TopSpaceNorm X), ( TopSpaceNorm Y);

      assume

       A1: f = ft;

      

       A2: (f | the carrier of X) = f by RELSET_1: 19;

      hereby

        assume

         A3: f is_continuous_on the carrier of X;

        now

          let xt be Point of ( TopSpaceNorm X);

          reconsider x = xt as Point of X;

          (f | the carrier of X) is_continuous_in x by A3, NFCONT_1:def 7;

          hence ft is_continuous_at xt by A1, A2, Th18;

        end;

        hence ft is continuous by TMAP_1: 44;

      end;

      assume

       A4: ft is continuous;

       A5:

      now

        let x be Point of X;

        assume x in the carrier of X;

        reconsider xt = x as Point of ( TopSpaceNorm X);

        ft is_continuous_at xt by A4, TMAP_1: 44;

        hence (f | the carrier of X) is_continuous_in x by A1, A2, Th18;

      end;

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

      hence thesis by A5, NFCONT_1:def 7;

    end;

    begin

    definition

      let X be RealNormSpace;

      :: NORMSP_2:def4

      func LinearTopSpaceNorm X -> strict non empty RLTopStruct means

      : Def4: the carrier of it = the carrier of X & ( 0. it ) = ( 0. X) & the addF of it = the addF of X & the Mult of it = the Mult of X & the topology of it = the topology of ( TopSpaceNorm X);

      existence

      proof

        reconsider TP = the topology of ( TopSpaceNorm X) as Subset-Family of X;

        take RLTopStruct (# the carrier of X, ( 0. X), the addF of X, the Mult of X, TP #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let X be RealNormSpace;

      cluster ( LinearTopSpaceNorm X) -> add-continuous Mult-continuous TopSpace-like Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      correctness

      proof

        thus ( LinearTopSpaceNorm X) is add-continuous

        proof

          let x1,x2 be Point of ( LinearTopSpaceNorm X);

          reconsider z2 = x2 as Element of ( MetricSpaceNorm X) by Def4;

          reconsider z1 = x1 as Element of ( MetricSpaceNorm X) by Def4;

          reconsider z12 = (x1 + x2) as Element of ( MetricSpaceNorm X) by Def4;

          let V be Subset of ( LinearTopSpaceNorm X);

          assume that

           A1: V is open and

           A2: (x1 + x2) in V;

          V in the topology of ( LinearTopSpaceNorm X) by A1;

          then V in the topology of ( TopSpaceNorm X) by Def4;

          then

          consider r be Real such that

           A3: r > 0 and

           A4: ( Ball (z12,r)) c= V by A2, PCOMPS_1:def 4;

          set r2 = (r / 2);

          

           A5: 0 < r2 by A3, XREAL_1: 215;

          reconsider V1 = ( Ball (z1,(r / 2))), V2 = ( Ball (z2,(r / 2))) as Subset of ( LinearTopSpaceNorm X) by Def4;

          

           A6: (V1 + V2) c= V

          proof

            let w be object;

            assume w in (V1 + V2);

            then

            consider v,u be VECTOR of ( LinearTopSpaceNorm X) such that

             A7: w = (v + u) and

             A8: v in V1 & u in V2;

            reconsider v1 = v, u1 = u as Element of ( MetricSpaceNorm X) by Def4;

            reconsider w1 = w as Element of ( MetricSpaceNorm X) by A7, Def4;

            reconsider zz12 = (x1 + x2), zz1 = x1, zz2 = x2, vv1 = v, uu1 = u as Point of X by Def4;

            

             A9: ||.((zz1 - vv1) + (zz2 - uu1)).|| <= ( ||.(zz1 - vv1).|| + ||.(zz2 - uu1).||) & ||.(zz1 - vv1).|| = ( dist (z1,v1)) by Def1, NORMSP_1:def 1;

            ( dist (z1,v1)) < (r / 2) & ( dist (z2,u1)) < (r / 2) by A8, METRIC_1: 11;

            then

             A10: (( dist (z1,v1)) + ( dist (z2,u1))) < ((r / 2) + (r / 2)) by XREAL_1: 8;

            reconsider ww1 = w as Point of X by A7, Def4;

            

             A11: ||.(zz2 - uu1).|| = ( dist (z2,u1)) by Def1;

            ( dist (z12,w1)) = ||.(zz12 - ww1).|| by Def1

            .= ||.((zz1 + zz2) - ww1).|| by Def4

            .= ||.((zz1 + zz2) - (vv1 + uu1)).|| by A7, Def4

            .= ||.((zz1 + zz2) + (( - uu1) + ( - vv1))).|| by RLVECT_1: 31

            .= ||.(((zz1 + zz2) + ( - vv1)) + ( - uu1)).|| by RLVECT_1:def 3

            .= ||.(((zz1 + ( - vv1)) + zz2) + ( - uu1)).|| by RLVECT_1:def 3

            .= ||.((zz1 + ( - vv1)) + (zz2 + ( - uu1))).|| by RLVECT_1:def 3;

            then ( dist (z12,w1)) < r by A9, A11, A10, XXREAL_0: 2;

            then w1 in ( Ball (z12,r)) by METRIC_1: 11;

            hence thesis by A4;

          end;

          ( dist (z2,z2)) = 0 by METRIC_1: 1;

          then

           A12: x2 in V2 by A5, METRIC_1: 11;

          ( Ball (z2,(r / 2))) in the topology of ( TopSpaceNorm X) by PCOMPS_1: 29;

          then ( Ball (z2,(r / 2))) in the topology of ( LinearTopSpaceNorm X) by Def4;

          then

           A13: V2 is open;

          ( Ball (z1,(r / 2))) in the topology of ( TopSpaceNorm X) by PCOMPS_1: 29;

          then ( Ball (z1,(r / 2))) in the topology of ( LinearTopSpaceNorm X) by Def4;

          then

           A14: V1 is open;

          ( dist (z1,z1)) = 0 by METRIC_1: 1;

          then x1 in V1 by A5, METRIC_1: 11;

          hence thesis by A14, A13, A12, A6;

        end;

         A15:

        now

          let a,b be Real;

          let v be VECTOR of ( LinearTopSpaceNorm X);

          reconsider v1 = v as VECTOR of X by Def4;

          (a * v) = (a * v1) & (b * v) = (b * v1) by Def4;

          then

           A16: ((a * v1) + (b * v1)) = ((a * v) + (b * v)) by Def4;

          ((a + b) * v) = ((a + b) * v1) by Def4;

          hence ((a + b) * v) = ((a * v) + (b * v)) by A16, RLVECT_1:def 6;

        end;

        thus ( LinearTopSpaceNorm X) is Mult-continuous

        proof

          let a be Real, x be Point of ( LinearTopSpaceNorm X), V be Subset of ( LinearTopSpaceNorm X) such that

           A17: V is open and

           A18: (a * x) in V;

          reconsider z = x, az = (a * x) as Element of ( MetricSpaceNorm X) by Def4;

          V in the topology of ( LinearTopSpaceNorm X) by A17;

          then V in the topology of ( TopSpaceNorm X) by Def4;

          then

          consider r0 be Real such that

           A19: r0 > 0 and

           A20: ( Ball (az,r0)) c= V by A18, PCOMPS_1:def 4;

          set r = (r0 / 2);

          r > 0 by A19, XREAL_1: 215;

          then

           A21: 0 < (r / 2) by XREAL_1: 215;

          reconsider z1 = z as Point of X;

          set r2 = ( min (((r / 2) / ((1 + ||.z1.||) + |.a.|)),1));

          reconsider W = ( Ball (z,r2)) as Subset of ( LinearTopSpaceNorm X) by Def4;

          

           A22: (r0 / 2) < (r0 / 1) by A19, XREAL_1: 76;

          

           A23: for s be Real st |.(s - a).| < r2 holds (s * W) c= V

          proof

            let s be Real;

            assume |.(s - a).| < r2;

            then

             A24: |.(a - s).| <= r2 by COMPLEX1: 60;

            thus (s * W) c= V

            proof

              let w be object;

              assume w in (s * W);

              then

              consider v be VECTOR of ( LinearTopSpaceNorm X) such that

               A25: w = (s * v) and

               A26: v in W;

              reconsider v1 = v as Element of ( MetricSpaceNorm X) by Def4;

              

               A27: ( dist (z,v1)) < r2 by A26, METRIC_1: 11;

              reconsider w1 = w as Element of ( MetricSpaceNorm X) by A25, Def4;

              reconsider zza = (a * x), zz = x, vv1 = v as Point of X by Def4;

              

               A28: ||.(zz - vv1).|| = ( dist (z,v1)) by Def1;

              r2 <= 1 by XXREAL_0: 17;

              then ||.(zz - vv1).|| <= 1 by A28, A27, XXREAL_0: 2;

              then ||.(vv1 - zz).|| <= 1 by NORMSP_1: 7;

              then

               A29: ( ||.zz.|| + ||.(vv1 - zz).||) <= ( ||.zz.|| + 1) by XREAL_1: 6;

              (zz + (vv1 - zz)) = (vv1 - (zz - zz)) by RLVECT_1: 29

              .= (vv1 - ( 0. X)) by RLVECT_1: 15

              .= vv1 by RLVECT_1: 13;

              then ||.vv1.|| <= ( ||.zz.|| + ||.(vv1 - zz).||) by NORMSP_1:def 1;

              then

               A30: ||.vv1.|| <= ( ||.zz.|| + 1) by A29, XXREAL_0: 2;

              

               A31: 0 <= (1 + ||.z1.||) by NORMSP_1: 4, XREAL_1: 39;

              then

               A32: (r2 * ( ||.zz.|| + 1)) <= (((r / 2) / ((1 + ||.z1.||) + |.a.|)) * ( ||.zz.|| + 1)) by XREAL_1: 64, XXREAL_0: 17;

               0 <= |.(a - s).| & 0 <= ||.vv1.|| by COMPLEX1: 46, NORMSP_1: 4;

              then ( |.(a - s).| * ||.vv1.||) <= (r2 * ( ||.zz.|| + 1)) by A24, A30, XREAL_1: 66;

              then ( |.(a - s).| * ||.vv1.||) <= (((r / 2) / ((1 + ||.z1.||) + |.a.|)) * ( ||.z1.|| + 1)) by A32, XXREAL_0: 2;

              then

               A33: ( |.(a - s).| * ||.vv1.||) <= ((( ||.z1.|| + 1) / ((1 + ||.z1.||) + |.a.|)) * (r / 2)) by XCMPLX_1: 75;

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

              then ( 0 + (1 + ||.z1.||)) <= ( |.a.| + (1 + ||.z1.||)) by XREAL_1: 6;

              then (( ||.z1.|| + 1) / ((1 + ||.z1.||) + |.a.|)) <= 1 by A31, XREAL_1: 183;

              then ((( ||.z1.|| + 1) / ((1 + ||.z1.||) + |.a.|)) * (r / 2)) <= (1 * (r / 2)) by A19, XREAL_1: 64;

              then

               A34: ( |.(a - s).| * ||.vv1.||) <= (r / 2) by A33, XXREAL_0: 2;

              reconsider ww1 = w as Point of X by A25, Def4;

              ((a * (zz - vv1)) - ((s - a) * vv1)) = (((a * zz) - (a * vv1)) - ((s - a) * vv1)) by RLVECT_1: 34

              .= (((a * zz) - (a * vv1)) - ((s * vv1) - (a * vv1))) by RLVECT_1: 35

              .= ((a * zz) - (((s * vv1) - (a * vv1)) + (a * vv1))) by RLVECT_1: 27

              .= ((a * zz) - ((s * vv1) - ((a * vv1) - (a * vv1)))) by RLVECT_1: 29

              .= ((a * zz) - ((s * vv1) - ( 0. X))) by RLVECT_1: 15

              .= ((a * zz) - (s * vv1)) by RLVECT_1: 13;

              then ||.((a * zz) - (s * vv1)).|| <= ( ||.(a * (zz - vv1)).|| + ||.((s - a) * vv1).||) by NORMSP_1: 3;

              then ||.((a * zz) - (s * vv1)).|| <= (( |.a.| * ||.(zz - vv1).||) + ||.((s - a) * vv1).||) by NORMSP_1:def 1;

              then ||.((a * zz) - (s * vv1)).|| <= (( |.a.| * ||.(zz - vv1).||) + ( |.(s - a).| * ||.vv1.||)) by NORMSP_1:def 1;

              then

               A35: ||.((a * zz) - (s * vv1)).|| <= (( |.a.| * ||.(zz - vv1).||) + ( |.(a - s).| * ||.vv1.||)) by COMPLEX1: 60;

              

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

              then

               A37: (r2 * |.a.|) <= (((r / 2) / ((1 + ||.z1.||) + |.a.|)) * |.a.|) by XREAL_1: 64, XXREAL_0: 17;

               0 <= (1 + ||.z1.||) by NORMSP_1: 4, XREAL_1: 39;

              then ( 0 + |.a.|) <= ((1 + ||.z1.||) + |.a.|) by XREAL_1: 6;

              then ( |.a.| / ((1 + ||.z1.||) + |.a.|)) <= 1 by A36, XREAL_1: 183;

              then

               A38: (( |.a.| / ((1 + ||.z1.||) + |.a.|)) * (r / 2)) <= (1 * (r / 2)) by A19, XREAL_1: 64;

              ( ||.(zz - vv1).|| * |.a.|) <= (r2 * |.a.|) by A28, A27, A36, XREAL_1: 64;

              then ( |.a.| * ||.(zz - vv1).||) <= ( |.a.| * ((r / 2) / ((1 + ||.z1.||) + |.a.|))) by A37, XXREAL_0: 2;

              then ( |.a.| * ||.(zz - vv1).||) <= (( |.a.| / ((1 + ||.z1.||) + |.a.|)) * (r / 2)) by XCMPLX_1: 75;

              then ( |.a.| * ||.(zz - vv1).||) <= (r / 2) by A38, XXREAL_0: 2;

              then

               A39: (( |.a.| * ||.(zz - vv1).||) + ( |.(a - s).| * ||.vv1.||)) <= ((r / 2) + (r / 2)) by A34, XREAL_1: 7;

              ( dist (az,w1)) = ||.(zza - ww1).|| by Def1

              .= ||.((a * zz) - ww1).|| by Def4

              .= ||.((a * zz) - (s * vv1)).|| by A25, Def4;

              then ( dist (az,w1)) <= r by A35, A39, XXREAL_0: 2;

              then ( dist (az,w1)) < r0 by A22, XXREAL_0: 2;

              then w1 in ( Ball (az,r0)) by METRIC_1: 11;

              hence thesis by A20;

            end;

          end;

           0 <= ||.z1.|| & 0 <= |.a.| by COMPLEX1: 46, NORMSP_1: 4;

          then ( 0 / ((1 + ||.z1.||) + |.a.|)) < ((r / 2) / ((1 + ||.z1.||) + |.a.|)) by A21, XREAL_1: 74;

          then

           A40: 0 < r2 by XXREAL_0: 15;

          ( Ball (z,r2)) in the topology of ( TopSpaceNorm X) by PCOMPS_1: 29;

          then ( Ball (z,r2)) in the topology of ( LinearTopSpaceNorm X) by Def4;

          then

           A41: W is open;

          ( dist (z,z)) = 0 by METRIC_1: 1;

          then x in W by A40, METRIC_1: 11;

          hence thesis by A41, A40, A23;

        end;

        thus ( LinearTopSpaceNorm X) is TopSpace-like

        proof

          set LTSN = ( LinearTopSpaceNorm X);

          

           A42: the topology of LTSN = the topology of ( TopSpaceNorm X) by Def4;

          then

           A43: for a,b be Subset of LTSN st a in the topology of LTSN & b in the topology of LTSN holds (a /\ b) in the topology of LTSN by PRE_TOPC:def 1;

          the carrier of LTSN = the carrier of ( TopSpaceNorm X) by Def4;

          then the carrier of LTSN in the topology of LTSN & for a be Subset-Family of LTSN st a c= the topology of LTSN holds ( union a) in the topology of LTSN by A42, PRE_TOPC:def 1;

          hence thesis by A43;

        end;

        thus ( LinearTopSpaceNorm X) is Abelian

        proof

          let v,w be VECTOR of ( LinearTopSpaceNorm X);

          reconsider v1 = v, w1 = w as VECTOR of X by Def4;

          

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

          .= (w1 + v1)

          .= (w + v) by Def4;

        end;

        thus ( LinearTopSpaceNorm X) is add-associative

        proof

          let v,w,x be VECTOR of ( LinearTopSpaceNorm X);

          reconsider v1 = v, w1 = w, x1 = x as VECTOR of X by Def4;

          

           A44: (w + x) = (w1 + x1) by Def4;

          (v + w) = (v1 + w1) by Def4;

          

          hence ((v + w) + x) = ((v1 + w1) + x1) by Def4

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

          .= (v + (w + x)) by A44, Def4;

        end;

        thus ( LinearTopSpaceNorm X) is right_zeroed

        proof

          let v be VECTOR of ( LinearTopSpaceNorm X);

          reconsider v1 = v as VECTOR of X by Def4;

          ( 0. ( LinearTopSpaceNorm X)) = ( 0. X) by Def4;

          

          hence (v + ( 0. ( LinearTopSpaceNorm X))) = (v1 + ( 0. X)) by Def4

          .= v by RLVECT_1:def 4;

        end;

        thus ( LinearTopSpaceNorm X) is right_complementable

        proof

          let v be VECTOR of ( LinearTopSpaceNorm X);

          reconsider v1 = v as VECTOR of X by Def4;

          reconsider w = ( - v1) as VECTOR of ( LinearTopSpaceNorm X) by Def4;

          take w;

          

          thus (v + w) = (v1 - v1) by Def4

          .= ( 0. X) by RLVECT_1: 15

          .= ( 0. ( LinearTopSpaceNorm X)) by Def4;

        end;

         A45:

        now

          let a,b be Real;

          let v be VECTOR of ( LinearTopSpaceNorm X);

          reconsider v1 = v as VECTOR of X by Def4;

          (b * v) = (b * v1) by Def4;

          then (a * (b * v1)) = (a * (b * v)) by Def4;

          then ((a * b) * v1) = (a * (b * v)) by RLVECT_1:def 7;

          hence ((a * b) * v) = (a * (b * v)) by Def4;

        end;

         A46:

        now

          let a be Real;

          let v,w be VECTOR of ( LinearTopSpaceNorm X);

          reconsider v1 = v, w1 = w as VECTOR of X by Def4;

          (a * v) = (a * v1) & (a * w) = (a * w1) by Def4;

          then

           A47: ((a * v1) + (a * w1)) = ((a * v) + (a * w)) by Def4;

          (v + w) = (v1 + w1) by Def4;

          then (a * (v + w)) = (a * (v1 + w1)) by Def4;

          hence (a * (v + w)) = ((a * v) + (a * w)) by A47, RLVECT_1:def 5;

        end;

        now

          let v be VECTOR of ( LinearTopSpaceNorm X);

          reconsider v1 = v as VECTOR of X by Def4;

          

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

          .= v by RLVECT_1:def 8;

        end;

        hence ( LinearTopSpaceNorm X) is vector-distributive scalar-distributive scalar-associative scalar-unital by A46, A15, A45;

      end;

    end

    theorem :: NORMSP_2:20

    

     Th20: for X be RealNormSpace, V be Subset of ( TopSpaceNorm X), Vt be Subset of ( LinearTopSpaceNorm X) st V = Vt holds V is open iff Vt is open by Def4;

    theorem :: NORMSP_2:21

    

     Th21: for X be RealNormSpace, V be Subset of ( TopSpaceNorm X), Vt be Subset of ( LinearTopSpaceNorm X) st V = Vt holds V is closed iff Vt is closed

    proof

      let X be RealNormSpace, V be Subset of ( TopSpaceNorm X), Vt be Subset of ( LinearTopSpaceNorm X);

      assume V = Vt;

      then

       A1: (Vt ` ) = (V ` ) by Def4;

      Vt is closed iff (V ` ) is open by A1, Th20;

      hence thesis;

    end;

    theorem :: NORMSP_2:22

    for X be RealNormSpace, V be Subset of ( LinearTopSpaceNorm X) holds V is open iff for x be Point of X st x in V holds ex r be Real st r > 0 & { y where y be Point of X : ||.(x - y).|| < r } c= V

    proof

      let X be RealNormSpace, V be Subset of ( LinearTopSpaceNorm X);

      reconsider V0 = V as Subset of ( TopSpaceNorm X) by Def4;

      V is open iff V0 is open by Th20;

      hence thesis by Th7;

    end;

    theorem :: NORMSP_2:23

    for X be RealNormSpace, x be Point of X, r be Real, V be Subset of ( LinearTopSpaceNorm X) st V = { y where y be Point of X : ||.(x - y).|| < r } holds V is open

    proof

      let X be RealNormSpace, x be Point of X, r be Real, V be Subset of ( LinearTopSpaceNorm X);

      reconsider V0 = V as Subset of ( TopSpaceNorm X) by Def4;

      assume V = { y where y be Point of X : ||.(x - y).|| < r };

      then V0 is open by Th8;

      hence thesis by Th20;

    end;

    theorem :: NORMSP_2:24

    for X be RealNormSpace, x be Point of X, r be Real, V be Subset of ( TopSpaceNorm X) st V = { y where y be Point of X : ||.(x - y).|| <= r } holds V is closed

    proof

      let X be RealNormSpace, x be Point of X, r be Real, V be Subset of ( TopSpaceNorm X);

      assume

       A1: V = { y where y be Point of X : ||.(x - y).|| <= r };

      reconsider z = x as Element of ( MetricSpaceNorm X);

      ex t be Point of X st t = x & ( cl_Ball (z,r)) = { y where y be Point of X : ||.(t - y).|| <= r } by Th3;

      hence thesis by A1, TOPREAL6: 57;

    end;

    registration

      let X be RealNormSpace;

      cluster ( LinearTopSpaceNorm X) -> T_2;

      coherence

      proof

        let p,q be Point of ( LinearTopSpaceNorm X);

        

         A1: the topology of ( LinearTopSpaceNorm X) = the topology of ( TopSpaceNorm X) by Def4;

        reconsider p1 = p, q1 = q as Point of ( TopSpaceNorm X) by Def4;

        assume p <> q;

        then

        consider W1,V1 be Subset of ( TopSpaceNorm X) such that

         A2: W1 is open and

         A3: V1 is open and

         A4: p1 in W1 & q1 in V1 & W1 misses V1 by PRE_TOPC:def 10;

        reconsider W = W1, V = V1 as Subset of ( LinearTopSpaceNorm X) by Def4;

        V1 in the topology of ( TopSpaceNorm X) by A3;

        then

         A5: V is open by A1;

        W1 in the topology of ( TopSpaceNorm X) by A2;

        then W is open by A1;

        hence thesis by A4, A5;

      end;

      cluster ( LinearTopSpaceNorm X) -> sober;

      coherence by YELLOW_8: 22;

    end

    theorem :: NORMSP_2:25

    

     Th25: for X be RealNormSpace, S be Subset-Family of ( TopSpaceNorm X), St be Subset-Family of ( LinearTopSpaceNorm X), x be Point of ( TopSpaceNorm X), xt be Point of ( LinearTopSpaceNorm X) st S = St & x = xt holds St is Basis of xt iff S is Basis of x

    proof

      let X be RealNormSpace, S be Subset-Family of ( TopSpaceNorm X), St be Subset-Family of ( LinearTopSpaceNorm X), x be Point of ( TopSpaceNorm X), xt be Point of ( LinearTopSpaceNorm X);

      assume that

       A1: S = St and

       A2: x = xt;

      

       A3: ( Intersect S) = ( Intersect St) by A1, Def4;

      hereby

        assume

         A4: St is Basis of xt;

        then St c= the topology of ( LinearTopSpaceNorm X) by TOPS_2: 64;

        then

         A5: S c= the topology of ( TopSpaceNorm X) by A1, Def4;

         A6:

        now

          let U be Subset of ( TopSpaceNorm X) such that

           A7: U is open and

           A8: x in U;

          reconsider Ut = U as open Subset of ( LinearTopSpaceNorm X) by A7, Def4, Th20;

          consider Vt be Subset of ( LinearTopSpaceNorm X) such that

           A9: Vt in St & Vt c= Ut by A2, A4, A8, YELLOW_8:def 1;

          reconsider V = Vt as Subset of ( TopSpaceNorm X) by Def4;

          take V;

          thus V in S & V c= U by A1, A9;

        end;

        x in ( Intersect S) by A2, A3, A4, YELLOW_8:def 1;

        hence S is Basis of x by A5, A6, TOPS_2: 64, YELLOW_8:def 1;

      end;

      assume

       A10: S is Basis of x;

      then S c= the topology of ( TopSpaceNorm X) by TOPS_2: 64;

      then

       A11: St c= the topology of ( LinearTopSpaceNorm X) by A1, Def4;

       A12:

      now

        let Ut be Subset of ( LinearTopSpaceNorm X) such that

         A13: Ut is open and

         A14: xt in Ut;

        reconsider U = Ut as open Subset of ( TopSpaceNorm X) by A13, Def4, Th20;

        consider V be Subset of ( TopSpaceNorm X) such that

         A15: V in S & V c= U by A2, A10, A14, YELLOW_8:def 1;

        reconsider Vt = V as Subset of ( LinearTopSpaceNorm X) by Def4;

        take Vt;

        thus Vt in St & Vt c= Ut by A1, A15;

      end;

      xt in ( Intersect St) by A2, A3, A10, YELLOW_8:def 1;

      hence thesis by A11, A12, TOPS_2: 64, YELLOW_8:def 1;

    end;

    registration

      let X be RealNormSpace;

      cluster ( LinearTopSpaceNorm X) -> first-countable;

      coherence

      proof

        now

          let xt be Point of ( LinearTopSpaceNorm X);

          reconsider x = xt as Point of ( TopSpaceNorm X) by Def4;

          consider B be Basis of x such that

           A1: B is countable by FRECHET:def 2;

          reconsider Bt = B as Basis of xt by Th25, Def4;

          take Bt;

          thus Bt is countable by A1;

        end;

        hence thesis by FRECHET:def 2;

      end;

      cluster ( LinearTopSpaceNorm X) -> Frechet;

      coherence ;

      cluster ( LinearTopSpaceNorm X) -> sequential;

      coherence ;

    end

    theorem :: NORMSP_2:26

    

     Th26: for X be RealNormSpace, S be sequence of ( TopSpaceNorm X), St be sequence of ( LinearTopSpaceNorm X), x be Point of ( TopSpaceNorm X), xt be Point of ( LinearTopSpaceNorm X) st S = St & x = xt holds St is_convergent_to xt iff S is_convergent_to x

    proof

      let X be RealNormSpace, S be sequence of ( TopSpaceNorm X), St be sequence of ( LinearTopSpaceNorm X), x be Point of ( TopSpaceNorm X), xt be Point of ( LinearTopSpaceNorm X);

      assume that

       A1: S = St and

       A2: x = xt;

       A3:

      now

        assume

         A4: S is_convergent_to x;

        now

          let U1t be Subset of ( LinearTopSpaceNorm X) such that

           A5: U1t is open and

           A6: xt in U1t;

          reconsider U1 = U1t as open Subset of ( TopSpaceNorm X) by A5, Def4, Th20;

          consider n be Nat such that

           A7: for m be Nat st n <= m holds (S . m) in U1 by A2, A4, A6, FRECHET:def 3;

          take n;

          let m be Nat;

          assume n <= m;

          hence (St . m) in U1t by A1, A7;

        end;

        hence St is_convergent_to xt by FRECHET:def 3;

      end;

      now

        assume

         A8: St is_convergent_to xt;

        now

          let U1 be Subset of ( TopSpaceNorm X) such that

           A9: U1 is open and

           A10: x in U1;

          reconsider U1t = U1 as open Subset of ( LinearTopSpaceNorm X) by A9, Def4, Th20;

          consider n be Nat such that

           A11: for m be Nat st n <= m holds (St . m) in U1t by A2, A8, A10, FRECHET:def 3;

          take n;

          let m be Nat;

          assume n <= m;

          hence (S . m) in U1 by A1, A11;

        end;

        hence S is_convergent_to x by FRECHET:def 3;

      end;

      hence thesis by A3;

    end;

    theorem :: NORMSP_2:27

    

     Th27: for X be RealNormSpace, S be sequence of ( TopSpaceNorm X), St be sequence of ( LinearTopSpaceNorm X) st S = St holds St is convergent iff S is convergent

    proof

      let X be RealNormSpace, S be sequence of ( TopSpaceNorm X), St be sequence of ( LinearTopSpaceNorm X);

      assume

       A1: S = St;

       A2:

      now

        assume S is convergent;

        then

        consider x be Point of ( TopSpaceNorm X) such that

         A3: S is_convergent_to x by FRECHET:def 4;

        reconsider xt = x as Point of ( LinearTopSpaceNorm X) by Def4;

        St is_convergent_to xt by A1, A3, Th26;

        hence St is convergent by FRECHET:def 4;

      end;

      now

        assume St is convergent;

        then

        consider xt be Point of ( LinearTopSpaceNorm X) such that

         A4: St is_convergent_to xt by FRECHET:def 4;

        reconsider x = xt as Point of ( TopSpaceNorm X) by Def4;

        S is_convergent_to x by A1, A4, Th26;

        hence S is convergent by FRECHET:def 4;

      end;

      hence thesis by A2;

    end;

    theorem :: NORMSP_2:28

    

     Th28: for X be RealNormSpace, S be sequence of ( TopSpaceNorm X), St be sequence of ( LinearTopSpaceNorm X) st S = St & St is convergent holds ( Lim S) = ( Lim St) & ( lim S) = ( lim St)

    proof

      let X be RealNormSpace, S be sequence of ( TopSpaceNorm X), St be sequence of ( LinearTopSpaceNorm X);

      assume that

       A1: S = St and

       A2: St is convergent;

      

       A3: S is convergent by A1, A2, Th27;

      then

      consider x be Point of ( TopSpaceNorm X) such that

       A4: S is_convergent_to x by FRECHET:def 4;

      reconsider xxt = x as Point of ( LinearTopSpaceNorm X) by Def4;

      St is_convergent_to xxt by A1, A4, Th26;

      

      then

       A5: ( lim St) = xxt by FRECHET2: 25

      .= ( lim S) by A4, FRECHET2: 25;

      reconsider Sn = S as sequence of X;

      consider xt be Point of ( LinearTopSpaceNorm X) such that

       A6: ( Lim St) = {xt} by A2, FRECHET2: 24;

      xt in {xt} by TARSKI:def 1;

      then St is_convergent_to xt by A6, FRECHET:def 5;

      

      then ( Lim St) = {( lim St)} by A6, FRECHET2: 25

      .= {( lim Sn)} by A3, A5, Th14

      .= ( Lim S) by A3, Th14;

      hence thesis by A5;

    end;

    theorem :: NORMSP_2:29

    for X be RealNormSpace, S be sequence of X, St be sequence of ( LinearTopSpaceNorm X), x be Point of X, xt be Point of ( LinearTopSpaceNorm X) st S = St & x = xt holds St is_convergent_to xt iff for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((S . n) - x).|| < r

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( LinearTopSpaceNorm X), x be Point of X, xt be Point of ( LinearTopSpaceNorm X);

      reconsider xxt = xt as Point of ( TopSpaceNorm X) by Def4;

      assume

       A1: S = St & x = xt;

      the carrier of ( LinearTopSpaceNorm X) = the carrier of ( TopSpaceNorm X) by Def4;

      then

      reconsider SSt = St as sequence of ( TopSpaceNorm X);

      St is_convergent_to xt iff SSt is_convergent_to xxt by Th26;

      hence thesis by A1, Th12;

    end;

    theorem :: NORMSP_2:30

    for X be RealNormSpace, S be sequence of X, St be sequence of ( LinearTopSpaceNorm X) st S = St holds St is convergent iff S is convergent

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( LinearTopSpaceNorm X);

      assume

       A1: S = St;

      the carrier of ( LinearTopSpaceNorm X) = the carrier of ( TopSpaceNorm X) by Def4;

      then

      reconsider SSt = St as sequence of ( TopSpaceNorm X);

      St is convergent iff SSt is convergent by Th27;

      hence thesis by A1, Th13;

    end;

    theorem :: NORMSP_2:31

    for X be RealNormSpace, S be sequence of X, St be sequence of ( LinearTopSpaceNorm X) st S = St & St is convergent holds ( Lim St) = {( lim S)} & ( lim St) = ( lim S)

    proof

      let X be RealNormSpace, S be sequence of X, St be sequence of ( LinearTopSpaceNorm X);

      assume that

       A1: S = St and

       A2: St is convergent;

      the carrier of ( LinearTopSpaceNorm X) = the carrier of ( TopSpaceNorm X) by Def4;

      then

      reconsider SSt = St as sequence of ( TopSpaceNorm X);

      SSt is convergent by A2, Th27;

      then ( Lim SSt) = {( lim S)} & ( lim SSt) = ( lim S) by A1, Th14;

      hence thesis by A2, Th28;

    end;

    theorem :: NORMSP_2:32

    for X be RealNormSpace, V be Subset of X, Vt be Subset of ( LinearTopSpaceNorm X) st V = Vt holds V is closed iff Vt is closed

    proof

      let X be RealNormSpace, V be Subset of X, Vt be Subset of ( LinearTopSpaceNorm X);

      reconsider VVt = Vt as Subset of ( TopSpaceNorm X) by Def4;

      assume

       A1: V = Vt;

      Vt is closed iff VVt is closed by Th21;

      hence thesis by A1, Th15;

    end;

    theorem :: NORMSP_2:33

    for X be RealNormSpace, V be Subset of X, Vt be Subset of ( LinearTopSpaceNorm X) st V = Vt holds V is open iff Vt is open

    proof

      let X be RealNormSpace, V be Subset of X, Vt be Subset of ( LinearTopSpaceNorm X);

      reconsider VVt = Vt as Subset of ( TopSpaceNorm X) by Def4;

      assume

       A1: V = Vt;

      Vt is open iff VVt is open by Th20;

      hence thesis by A1, Th16;

    end;

    theorem :: NORMSP_2:34

    

     Th34: for X be RealNormSpace, U be Subset of ( TopSpaceNorm X), Ut be Subset of ( LinearTopSpaceNorm X), x be Point of ( TopSpaceNorm X), xt be Point of ( LinearTopSpaceNorm X) st U = Ut & x = xt holds U is a_neighborhood of x iff Ut is a_neighborhood of xt

    proof

      let X be RealNormSpace, U be Subset of ( TopSpaceNorm X), Ut be Subset of ( LinearTopSpaceNorm X), x be Point of ( TopSpaceNorm X), xt be Point of ( LinearTopSpaceNorm X);

      assume that

       A1: U = Ut and

       A2: x = xt;

      hereby

        assume U is a_neighborhood of x;

        then

        consider V be Subset of ( TopSpaceNorm X) such that

         A3: V is open and

         A4: V c= U and

         A5: x in V by CONNSP_2: 6;

        reconsider Vt = V as open Subset of ( LinearTopSpaceNorm X) by A3, Def4, Th20;

        Vt c= Ut by A1, A4;

        hence Ut is a_neighborhood of xt by A2, A5, CONNSP_2: 6;

      end;

      assume Ut is a_neighborhood of xt;

      then

      consider Vt be Subset of ( LinearTopSpaceNorm X) such that

       A6: Vt is open and

       A7: Vt c= Ut and

       A8: xt in Vt by CONNSP_2: 6;

      reconsider V = Vt as open Subset of ( TopSpaceNorm X) by A6, Def4, Th20;

      V c= U by A1, A7;

      hence thesis by A2, A8, CONNSP_2: 6;

    end;

    theorem :: NORMSP_2:35

    

     Th35: for X,Y be RealNormSpace, f be Function of ( TopSpaceNorm X), ( TopSpaceNorm Y), ft be Function of ( LinearTopSpaceNorm X), ( LinearTopSpaceNorm Y), x be Point of ( TopSpaceNorm X), xt be Point of ( LinearTopSpaceNorm X) st f = ft & x = xt holds f is_continuous_at x iff ft is_continuous_at xt

    proof

      let X,Y be RealNormSpace, f be Function of ( TopSpaceNorm X), ( TopSpaceNorm Y), ft be Function of ( LinearTopSpaceNorm X), ( LinearTopSpaceNorm Y), x be Point of ( TopSpaceNorm X), xt be Point of ( LinearTopSpaceNorm X);

      assume that

       A1: f = ft and

       A2: x = xt;

      hereby

        assume

         A3: f is_continuous_at x;

        now

          let Gt be a_neighborhood of (ft . xt);

          Gt is Subset of ( TopSpaceNorm Y) by Def4;

          then

          reconsider G = Gt as a_neighborhood of (f . x) by A1, A2, Th34;

          consider H be a_neighborhood of x such that

           A4: (f .: H) c= G by A3, TMAP_1:def 2;

          H is Subset of ( LinearTopSpaceNorm X) by Def4;

          then

          reconsider Ht = H as a_neighborhood of xt by A2, Th34;

          take Ht;

          thus (ft .: Ht) c= Gt by A1, A4;

        end;

        hence ft is_continuous_at xt by TMAP_1:def 2;

      end;

      assume

       A5: ft is_continuous_at xt;

      now

        let G be a_neighborhood of (f . x);

        G is Subset of ( LinearTopSpaceNorm Y) by Def4;

        then

        reconsider Gt = G as a_neighborhood of (ft . xt) by A1, A2, Th34;

        consider Ht be a_neighborhood of xt such that

         A6: (ft .: Ht) c= Gt by A5, TMAP_1:def 2;

        Ht is Subset of ( TopSpaceNorm X) by Def4;

        then

        reconsider H = Ht as a_neighborhood of x by A2, Th34;

        take H;

        thus (f .: H) c= G by A1, A6;

      end;

      hence thesis by TMAP_1:def 2;

    end;

    theorem :: NORMSP_2:36

    for X,Y be RealNormSpace, f be Function of ( TopSpaceNorm X), ( TopSpaceNorm Y), ft be Function of ( LinearTopSpaceNorm X), ( LinearTopSpaceNorm Y) st f = ft holds f is continuous iff ft is continuous

    proof

      let X,Y be RealNormSpace, f be Function of ( TopSpaceNorm X), ( TopSpaceNorm Y), ft be Function of ( LinearTopSpaceNorm X), ( LinearTopSpaceNorm Y);

      assume

       A1: f = ft;

      hereby

        assume

         A2: f is continuous;

        now

          let xt be Point of ( LinearTopSpaceNorm X);

          reconsider x = xt as Point of ( TopSpaceNorm X) by Def4;

          f is_continuous_at x by A2, TMAP_1: 44;

          hence ft is_continuous_at xt by A1, Th35;

        end;

        hence ft is continuous by TMAP_1: 44;

      end;

      assume

       A3: ft is continuous;

      now

        let x be Point of ( TopSpaceNorm X);

        reconsider xt = x as Point of ( LinearTopSpaceNorm X) by Def4;

        ft is_continuous_at xt by A3, TMAP_1: 44;

        hence f is_continuous_at x by A1, Th35;

      end;

      hence thesis by TMAP_1: 44;

    end;