normsp_4.miz



    begin

    definition

      let X be RealLinearSpace, A be Subset of X;

      :: NORMSP_4:def1

      func RAT_Sums (A) -> Subset of X equals { ( Sum l) where l be Linear_Combination of A : ( rng l) c= RAT };

      correctness

      proof

        set S = { ( Sum l) where l be Linear_Combination of A : ( rng l) c= RAT };

        now

          let x be object;

          assume x in S;

          then ex l be Linear_Combination of A st x = ( Sum l) & ( rng l) c= RAT ;

          hence x in ( [#] X);

        end;

        then S c= ( [#] X);

        hence thesis;

      end;

    end

    theorem :: NORMSP_4:1

    

     Th1: for V be RealNormSpace, V1 be SubRealNormSpace of V holds ( TopSpaceNorm V1) is SubSpace of ( TopSpaceNorm V)

    proof

      let V be RealNormSpace, V1 be SubRealNormSpace of V;

      

       A1: the carrier of ( MetricSpaceNorm V1) c= the carrier of ( MetricSpaceNorm V) by DUALSP01:def 16;

      for x,y be Point of ( MetricSpaceNorm V1) holds (the distance of ( MetricSpaceNorm V1) . (x,y)) = (the distance of ( MetricSpaceNorm V) . (x,y))

      proof

        let x,y be Point of ( MetricSpaceNorm V1);

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

        reconsider x2 = x, y2 = y as Point of V by A1;

        ( - y1) = (( - 1) * y1) by RLVECT_1: 16

        .= (( - 1) * y2) by NORMSP_3: 28

        .= ( - y2) by RLVECT_1: 16;

        then

         A2: (x1 - y1) = (x2 - y2) by NORMSP_3: 28;

        

        thus (the distance of ( MetricSpaceNorm V1) . (x,y)) = ||.(x1 - y1).|| by NORMSP_2:def 1

        .= ||.(x2 - y2).|| by A2, NORMSP_3: 28

        .= (the distance of ( MetricSpaceNorm V) . (x,y)) by NORMSP_2:def 1;

      end;

      then ( MetricSpaceNorm V1) is SubSpace of ( MetricSpaceNorm V) by A1, TOPMETR:def 1;

      hence ( TopSpaceNorm V1) is SubSpace of ( TopSpaceNorm V) by TOPMETR: 13;

    end;

    theorem :: NORMSP_4:2

    

     Th2: for V be RealNormSpace, V1 be SubRealNormSpace of V holds ( LinearTopSpaceNorm V1) is SubSpace of ( LinearTopSpaceNorm V)

    proof

      let V be RealNormSpace, V1 be SubRealNormSpace of V;

      the carrier of ( LinearTopSpaceNorm V1) = the carrier of V1 & the carrier of ( LinearTopSpaceNorm V) = the carrier of V by NORMSP_2:def 4;

      then the TopStruct of ( LinearTopSpaceNorm V1) = the TopStruct of ( TopSpaceNorm V1) & the TopStruct of ( LinearTopSpaceNorm V) = the TopStruct of ( TopSpaceNorm V) by NORMSP_2:def 4;

      hence thesis by Th1, PRE_TOPC: 10;

    end;

    theorem :: NORMSP_4:3

    

     Th3: for X be RealNormSpace, Y,Z be SubRealNormSpace of X st ex A be Subset of X st A = the carrier of Y & ( Cl A) = the carrier of Z holds for D0 be Subset of Y, D be Subset of Z st D0 is dense & D0 = D holds D is dense

    proof

      let X be RealNormSpace, Y,Z be SubRealNormSpace of X;

      given A be Subset of X such that

       A1: A = the carrier of Y & ( Cl A) = the carrier of Z;

      let D0 be Subset of Y, D be Subset of Z;

      assume

       A2: D0 is dense & D0 = D;

      

       A3: the carrier of ( LinearTopSpaceNorm Z) = the carrier of Z & the carrier of ( LinearTopSpaceNorm Y) = the carrier of Y & the carrier of ( LinearTopSpaceNorm X) = the carrier of X by NORMSP_2:def 4;

      

       A4: ( LinearTopSpaceNorm Z) is SubSpace of ( LinearTopSpaceNorm X) & ( LinearTopSpaceNorm Y) is SubSpace of ( LinearTopSpaceNorm X) by Th2;

      for S be Subset of Z st S <> {} & S is open holds D meets S

      proof

        let S be Subset of Z;

        assume

         A5: S <> {} & S is open;

        reconsider SZL = S as Subset of ( LinearTopSpaceNorm Z) by NORMSP_2:def 4;

        reconsider SZT = SZL as Subset of ( TopSpaceNorm Z);

        SZT is open by A5, NORMSP_2: 16;

        then SZL is open by NORMSP_2: 20;

        then

        consider SXL be Subset of ( LinearTopSpaceNorm X) such that

         A6: SXL in the topology of ( LinearTopSpaceNorm X) & SZL = (SXL /\ ( [#] ( LinearTopSpaceNorm Z))) by A4, PRE_TOPC:def 4;

        reconsider SYL = (SXL /\ ( [#] ( LinearTopSpaceNorm Y))) as Subset of ( LinearTopSpaceNorm Y);

        reconsider SX = SXL as Subset of X by NORMSP_2:def 4;

        reconsider SXT = SXL as Subset of ( TopSpaceNorm X) by NORMSP_2:def 4;

        reconsider SY = SYL as Subset of Y by NORMSP_2:def 4;

        reconsider SYT = SYL as Subset of ( TopSpaceNorm Y) by NORMSP_2:def 4;

        SXL is open by A6;

        then SXT is open by NORMSP_2: 20;

        then

         A7: SX is open by NORMSP_2: 16;

        (SX /\ ( Cl A)) <> {} by A1, A5, A6, NORMSP_2:def 4;

        then

        consider v be object such that

         A8: v in (SX /\ ( Cl A)) by XBOOLE_0:def 1;

        v in SX & v in ( Cl A) by A8, XBOOLE_0:def 4;

        then SX meets A by A7, NORMSP_3: 5;

        then

         A9: SYL <> {} by A1, NORMSP_2:def 4;

        SYL is open by A4, A6, PRE_TOPC:def 4;

        then SYT is open by NORMSP_2: 20;

        then SY is open by NORMSP_2: 16;

        then

         A10: D0 meets SY by A2, A9, NORMSP_3: 17;

        SYL c= SZL by A1, A3, A6, NORMSP_3: 4, XBOOLE_1: 26;

        then (D /\ SYL) c= (D /\ SZL) by XBOOLE_1: 26;

        hence thesis by A2, A10;

      end;

      hence thesis by NORMSP_3: 17;

    end;

    theorem :: NORMSP_4:4

    

     Th4: for X be addLoopStr, A,B be Subset of X holds ex F be Function of (A + B), [:A, B:] st F is one-to-one

    proof

      let X be addLoopStr, A,B be Subset of X;

      set D = (A + B);

      defpred P[ object, object] means ex a,b be Point of X st $1 = (a + b) & a in A & b in B & $2 = [a, b];

      

       A2: for x be object st x in D holds ex y be object st y in [:A, B:] & P[x, y]

      proof

        let x be object;

        assume x in D;

        then x in { (a + b) where a,b be Element of X : a in A & b in B } by IDEAL_1:def 19;

        then

        consider a,b be Element of X such that

         A3: x = (a + b) & a in A & b in B;

        take y = [a, b];

        thus y in [:A, B:] by A3, ZFMISC_1: 87;

        thus P[x, y] by A3;

      end;

      consider F be Function of D, [:A, B:] such that

       A4: for x be object st x in D holds P[x, (F . x)] from FUNCT_2:sch 1( A2);

      take F;

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

      proof

        let x1,x2 be object;

        assume

         A5: x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2);

        then

         A6: ex a1,b1 be Point of X st x1 = (a1 + b1) & a1 in A & b1 in B & (F . x1) = [a1, b1] by A4;

        ex a2,b2 be Point of X st x2 = (a2 + b2) & a2 in A & b2 in B & (F . x2) = [a2, b2] by A4, A5;

        hence x1 = x2 by A5, A6;

      end;

      hence F is one-to-one;

    end;

    theorem :: NORMSP_4:5

    

     Th5: for X be addLoopStr, A,B be Subset of X st A is countable & B is countable holds (A + B) is countable

    proof

      let X be addLoopStr, A,B be Subset of X;

      assume

       A1: A is countable & B is countable;

      set D = (A + B);

      per cases ;

        suppose

         A2: not (A is non empty & B is non empty);

        now

          assume D <> {} ;

          then

          consider x be object such that

           A3: x in D by XBOOLE_0:def 1;

          D = { (a + b) where a,b be Point of X : a in A & b in B } by IDEAL_1:def 19;

          then ex a,b be Point of X st x = (a + b) & a in A & b in B by A3;

          hence contradiction by A2;

        end;

        hence thesis;

      end;

        suppose

         A4: A is non empty & B is non empty;

        consider F be Function of D, [:A, B:] such that

         A5: F is one-to-one by Th4;

        ( dom F) = D & ( rng F) c= [:A, B:] by A4, FUNCT_2:def 1;

        then

         A6: ( card D) c= ( card [:A, B:]) by A5, CARD_1: 10;

         [:A, B:] is countable by A1, CARD_4: 7;

        then ( card [:A, B:]) c= omega ;

        then ( card D) c= omega by A6;

        hence thesis;

      end;

    end;

    

     Lm6: for X be RealLinearSpace, v be Element of the carrier of X holds ( RAT_Sums {v}) is countable

    proof

      let X be RealLinearSpace, v be Element of the carrier of X;

      set D = ( RAT_Sums {v});

      defpred P[ object, object] means ex l be Linear_Combination of {v} st $1 = ( Sum l) & ( rng l) c= RAT & $2 = (l . v);

      

       A2: for x be object st x in D holds ex y be object st y in RAT & P[x, y]

      proof

        let x be object;

        assume x in D;

        then

        consider l be Linear_Combination of {v} such that

         A3: x = ( Sum l) & ( rng l) c= RAT ;

        take y = (l . v);

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

        hence y in RAT by A3, FUNCT_1: 3;

        thus P[x, y] by A3;

      end;

      consider F be Function of D, RAT such that

       A4: for x be object st x in D holds P[x, (F . x)] from FUNCT_2:sch 1( A2);

      now

        let x1,x2 be object;

        assume

         A5: x1 in ( dom F) & x2 in ( dom F) & (F . x1) = (F . x2);

        then

        consider l1 be Linear_Combination of {v} such that

         A6: x1 = ( Sum l1) & ( rng l1) c= RAT & (F . x1) = (l1 . v) by A4;

        consider l2 be Linear_Combination of {v} such that

         A7: x2 = ( Sum l2) & ( rng l2) c= RAT & (F . x2) = (l2 . v) by A4, A5;

        x1 = ((l1 . v) * v) & x2 = ((l2 . v) * v) by A6, A7, RLVECT_2: 32;

        hence x1 = x2 by A5, A6, A7;

      end;

      then

       A8: F is one-to-one;

      

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

      ( rng F) is countable;

      then

       A10: ( card D) c= ( card RAT ) by A8, A9, CARD_1: 10;

      ( card RAT ) c= omega by CARD_3:def 14;

      then ( card D) c= omega by A10;

      hence D is countable;

    end;

    theorem :: NORMSP_4:6

    

     Th7: for X be non empty addLoopStr, A,B be Subset of X, l1 be Linear_Combination of A, l2 be Linear_Combination of B st A misses B holds ex l be Linear_Combination of (A \/ B) st ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) & l = (l1 + l2)

    proof

      let X be non empty addLoopStr, A,B be Subset of X, l1 be Linear_Combination of A, l2 be Linear_Combination of B;

      assume

       A1: A misses B;

      

       A2: ( Carrier l1) c= A & ( Carrier l2) c= B by RLVECT_2:def 6;

      defpred P[ object, object] means ($1 in ( Carrier l1) implies $2 = (l1 . $1)) & ($1 in ( Carrier l2) implies $2 = (l2 . $1)) & ( not $1 in ( Carrier l1) & not $1 in ( Carrier l2) implies $2 = 0 );

       A4:

      now

        let x be object;

        assume x in the carrier of X;

        thus ex y be object st y in REAL & P[x, y]

        proof

          per cases by A1, A2, XBOOLE_0: 3;

            suppose

             A5: x in ( Carrier l1) & not x in ( Carrier l2);

            take y = (l1 . x);

            thus y in REAL & P[x, y] by A5, FUNCT_2: 5;

          end;

            suppose

             A6: not x in ( Carrier l1) & x in ( Carrier l2);

            take y = (l2 . x);

            thus y in REAL & P[x, y] by A6, FUNCT_2: 5;

          end;

            suppose

             A7: not x in ( Carrier l1) & not x in ( Carrier l2);

            take y = 0 ;

            thus y in REAL & P[x, y] by A7, XREAL_0:def 1;

          end;

        end;

      end;

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

       A8: for x be object st x in the carrier of X holds P[x, (l . x)] from FUNCT_2:sch 1( A4);

      reconsider l as Element of ( Funcs (the carrier of X, REAL )) by FUNCT_2: 8;

      reconsider T = (( Carrier l1) \/ ( Carrier l2)) as finite Subset of X;

      for x be Element of X st not x in T holds (l . x) = 0

      proof

        let x be Element of X;

        assume not x in T;

        then not x in ( Carrier l1) & not x in ( Carrier l2) by XBOOLE_0:def 3;

        hence (l . x) = 0 by A8;

      end;

      then

      reconsider l as Linear_Combination of X by RLVECT_2:def 3;

      now

        let x be object;

        assume x in ( Carrier l);

        then

        consider p be Element of X such that

         A9: x = p & (l . p) <> 0 ;

        x in ( Carrier l1) or x in ( Carrier l2) by A8, A9;

        hence x in (( Carrier l1) \/ ( Carrier l2)) by XBOOLE_0:def 3;

      end;

      then

       A10: ( Carrier l) c= (( Carrier l1) \/ ( Carrier l2));

      now

        let x be object;

        assume x in (( Carrier l1) \/ ( Carrier l2));

        per cases by XBOOLE_0:def 3;

          suppose

           A11: x in ( Carrier l1);

          then

          consider p be Element of X such that

           A12: x = p & (l1 . p) <> 0 ;

          (l . x) <> 0 by A8, A11, A12;

          hence x in ( Carrier l) by A12;

        end;

          suppose

           A13: x in ( Carrier l2);

          then

          consider p be Element of X such that

           A14: x = p & (l2 . p) <> 0 ;

          (l . x) <> 0 by A8, A13, A14;

          hence x in ( Carrier l) by A14;

        end;

      end;

      then

       A15: (( Carrier l1) \/ ( Carrier l2)) c= ( Carrier l);

      then

       A16: ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) by A10;

      then

      reconsider l as Linear_Combination of (A \/ B) by A2, RLVECT_2:def 6, XBOOLE_1: 13;

      take l;

      thus ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) by A10, A15;

      for v be Element of X holds (l . v) = ((l1 . v) + (l2 . v))

      proof

        let v be Element of X;

        per cases by A10, XBOOLE_0:def 3;

          suppose

           A17: v in ( Carrier l1);

          then not v in ( Carrier l2) by A1, A2, XBOOLE_0: 3;

          then (l . v) = (l1 . v) & (l2 . v) = 0 by A8, A17;

          hence (l . v) = ((l1 . v) + (l2 . v));

        end;

          suppose

           A18: v in ( Carrier l2);

          then not v in ( Carrier l1) by A1, A2, XBOOLE_0: 3;

          then (l . v) = (l2 . v) & (l1 . v) = 0 by A8, A18;

          hence (l . v) = ((l1 . v) + (l2 . v));

        end;

          suppose

           A19: not v in ( Carrier l);

          then not v in ( Carrier l1) & not v in ( Carrier l2) by A16, XBOOLE_0:def 3;

          then (l1 . v) = 0 & (l2 . v) = 0 ;

          hence (l . v) = ((l1 . v) + (l2 . v)) by A19;

        end;

      end;

      hence l = (l1 + l2) by RLVECT_2:def 10;

    end;

    theorem :: NORMSP_4:7

    

     Th8: for X be non empty addLoopStr, A,B be Subset of X, l be Linear_Combination of (A \/ B) holds ex l1 be Linear_Combination of A st ( Carrier l1) = (( Carrier l) \ B) & for x be Element of X st x in ( Carrier l1) holds (l1 . x) = (l . x)

    proof

      let X be non empty addLoopStr, A,B be Subset of X, l be Linear_Combination of (A \/ B);

      reconsider T1 = (( Carrier l) \ B) as finite Subset of X;

      defpred P1[ object, object] means ($1 in T1 implies $2 = (l . $1)) & ( not $1 in T1 implies $2 = 0 );

       A1:

      now

        let x be object;

        assume x in the carrier of X;

        thus ex y be object st y in REAL & P1[x, y]

        proof

          per cases ;

            suppose

             A2: x in T1;

            take y = (l . x);

            thus y in REAL & P1[x, y] by A2, FUNCT_2: 5;

          end;

            suppose

             A3: not x in T1;

            take y = 0 ;

            thus y in REAL & P1[x, y] by A3, XREAL_0:def 1;

          end;

        end;

      end;

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

       A4: for x be object st x in the carrier of X holds P1[x, (l1 . x)] from FUNCT_2:sch 1( A1);

      reconsider l1 as Element of ( Funcs (the carrier of X, REAL )) by FUNCT_2: 8;

      for x be Element of X st not x in T1 holds (l1 . x) = 0 by A4;

      then

      reconsider l1 as Linear_Combination of X by RLVECT_2:def 3;

      now

        let x be object;

        assume x in ( Carrier l1);

        then ex v be Element of X st x = v & (l1 . v) <> 0 ;

        hence x in T1 by A4;

      end;

      then

       A5: ( Carrier l1) c= T1;

      now

        let x be object;

        assume

         A6: x in T1;

        then x in ( Carrier l) by XBOOLE_0:def 5;

        then (l . x) <> 0 by RLVECT_2: 19;

        then (l1 . x) <> 0 by A4, A6;

        hence x in ( Carrier l1) by A6;

      end;

      then

       A7: T1 c= ( Carrier l1);

      then

       A8: T1 = ( Carrier l1) by A5;

      T1 c= ( Carrier l) & ( Carrier l) c= (A \/ B) by RLVECT_2:def 6, XBOOLE_1: 36;

      then T1 c= (A \/ B) & T1 misses B by XBOOLE_1: 79;

      then

      reconsider l1 as Linear_Combination of A by A8, RLVECT_2:def 6, XBOOLE_1: 73;

      take l1;

      thus ( Carrier l1) = (( Carrier l) \ B) by A5, A7;

      thus for x be Element of X st x in ( Carrier l1) holds (l1 . x) = (l . x) by A4, A5;

    end;

    theorem :: NORMSP_4:8

    

     Th9: for X be non empty addLoopStr, A,B be Subset of X, l be Linear_Combination of (A \/ B) st A misses B holds ex l1 be Linear_Combination of A, l2 be Linear_Combination of B st ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) & l = (l1 + l2) & ( Carrier l1) = (( Carrier l) \ B) & ( Carrier l2) = (( Carrier l) \ A)

    proof

      let X be non empty addLoopStr, A,B be Subset of X, l be Linear_Combination of (A \/ B);

      assume

       A2: A misses B;

      consider l1 be Linear_Combination of A such that

       A3: ( Carrier l1) = (( Carrier l) \ B) & for x be Element of X st x in ( Carrier l1) holds (l1 . x) = (l . x) by Th8;

      consider l2 be Linear_Combination of B such that

       A4: ( Carrier l2) = (( Carrier l) \ A) & for x be Element of X st x in ( Carrier l2) holds (l2 . x) = (l . x) by Th8;

      take l1, l2;

      

       A5: (( Carrier l1) \/ ( Carrier l2)) = (( Carrier l) \ (A /\ B)) by A3, A4, XBOOLE_1: 54;

      hence (( Carrier l1) \/ ( Carrier l2)) = ( Carrier l) by A2;

      

       A6: ( Carrier l1) c= A & ( Carrier l2) c= B by RLVECT_2:def 6;

      now

        let x be Element of X;

        per cases by A2, A5, XBOOLE_0:def 3;

          suppose

           A7: x in ( Carrier l1);

          then not x in ( Carrier l2) by A2, A6, XBOOLE_0: 3;

          then (l1 . x) = (l . x) & (l2 . x) = 0 by A3, A7;

          hence (l . x) = ((l1 . x) + (l2 . x));

        end;

          suppose

           A8: x in ( Carrier l2);

          then not x in ( Carrier l1) by A2, A6, XBOOLE_0: 3;

          then (l1 . x) = 0 & (l2 . x) = (l . x) by A4, A8;

          hence (l . x) = ((l1 . x) + (l2 . x));

        end;

          suppose

           A9: not x in ( Carrier l);

          then not x in ( Carrier l1) & not x in ( Carrier l2) by A2, A5, XBOOLE_0:def 3;

          then (l . x) = 0 & (l1 . x) = 0 & (l2 . x) = 0 by A9;

          hence (l . x) = ((l1 . x) + (l2 . x));

        end;

      end;

      hence l = (l1 + l2) by RLVECT_2:def 10;

      thus thesis by A3, A4;

    end;

    theorem :: NORMSP_4:9

    

     Th10: for X be RealLinearSpace, A,B be Subset of X, l1 be Linear_Combination of A, l2 be Linear_Combination of B st ( rng l1) c= RAT & ( rng l2) c= RAT & A misses B holds ex l be Linear_Combination of (A \/ B) st ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) & ( rng l) c= RAT & ( Sum l) = (( Sum l1) + ( Sum l2))

    proof

      let X be RealLinearSpace, A,B be Subset of X, l1 be Linear_Combination of A, l2 be Linear_Combination of B;

      assume that

       A1: ( rng l1) c= RAT & ( rng l2) c= RAT and

       A2: A misses B;

      consider l be Linear_Combination of (A \/ B) such that

       A3: ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) & l = (l1 + l2) by A2, Th7;

      take l;

      thus ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) by A3;

      now

        let y be object;

        assume y in ( rng l);

        then

        consider x be object such that

         A4: x in ( dom l) & y = (l . x) by FUNCT_1:def 3;

        

         A5: x in the carrier of X by A4;

        

         A6: (l . x) = ((l1 . x) + (l2 . x)) by A3, A4, RLVECT_2:def 10;

        x in ( dom l1) & x in ( dom l2) by A5, FUNCT_2:def 1;

        then (l1 . x) in ( rng l1) & (l2 . x) in ( rng l2) by FUNCT_1: 3;

        hence y in RAT by A1, A4, A6, RAT_1:def 2;

      end;

      hence ( rng l) c= RAT ;

      thus ( Sum l) = (( Sum l1) + ( Sum l2)) by A3, RLVECT_3: 1;

    end;

    theorem :: NORMSP_4:10

    

     Th11: for X be RealLinearSpace, A,B be Subset of X, l be Linear_Combination of (A \/ B) st ( rng l) c= RAT & A misses B holds ex l1 be Linear_Combination of A, l2 be Linear_Combination of B st ( rng l1) c= RAT & ( rng l2) c= RAT & ( Sum l) = (( Sum l1) + ( Sum l2))

    proof

      let X be RealLinearSpace, A,B be Subset of X, l be Linear_Combination of (A \/ B);

      assume that

       A1: ( rng l) c= RAT and

       A3: A misses B;

      consider l1 be Linear_Combination of A, l2 be Linear_Combination of B such that

       A4: ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) & l = (l1 + l2) & ( Carrier l1) = (( Carrier l) \ B) & ( Carrier l2) = (( Carrier l) \ A) by A3, Th9;

      take l1, l2;

      

       A5: ( Carrier l1) c= A & ( Carrier l2) c= B by RLVECT_2:def 6;

      now

        let y be object;

        assume y in ( rng l1);

        then

        consider x be object such that

         A6: x in ( dom l1) & y = (l1 . x) by FUNCT_1:def 3;

        x in the carrier of X by A6;

        then x in ( dom l) & x in ( dom l2) by FUNCT_2:def 1;

        then

         A7: (l . x) in ( rng l) & (l2 . x) in ( rng l2) & (l . x) = ((l1 . x) + (l2 . x)) by A4, FUNCT_1: 3, RLVECT_2:def 10;

        per cases ;

          suppose x in ( Carrier l1);

          then not x in ( Carrier l2) by A3, A5, XBOOLE_0: 3;

          then (l2 . x) = 0 by A6;

          hence y in RAT by A1, A6, A7;

        end;

          suppose not x in ( Carrier l1);

          then (l1 . x) = 0 by A6;

          hence y in RAT by A6, RAT_1:def 2;

        end;

      end;

      hence ( rng l1) c= RAT ;

      now

        let y be object;

        assume y in ( rng l2);

        then

        consider x be object such that

         A8: x in ( dom l2) & y = (l2 . x) by FUNCT_1:def 3;

        x in the carrier of X by A8;

        then x in ( dom l) & x in ( dom l1) by FUNCT_2:def 1;

        then

         A9: (l . x) in ( rng l) & (l1 . x) in ( rng l1) & (l . x) = ((l1 . x) + (l2 . x)) by A4, FUNCT_1: 3, RLVECT_2:def 10;

        per cases ;

          suppose x in ( Carrier l2);

          then not x in ( Carrier l1) by A3, A5, XBOOLE_0: 3;

          then (l1 . x) = 0 by A8;

          hence y in RAT by A1, A8, A9;

        end;

          suppose not x in ( Carrier l2);

          then (l2 . x) = 0 by A8;

          hence y in RAT by A8, RAT_1:def 2;

        end;

      end;

      hence ( rng l2) c= RAT ;

      thus thesis by A4, RLVECT_3: 1;

    end;

    theorem :: NORMSP_4:11

    

     Th12: for X be RealLinearSpace, A,B be finite Subset of X st A misses B holds (( RAT_Sums A) + ( RAT_Sums B)) = ( RAT_Sums (A \/ B))

    proof

      let X be RealLinearSpace, A,B be finite Subset of X;

      assume

       A3: A misses B;

      set D1 = ( RAT_Sums A);

      set D2 = ( RAT_Sums B);

      set S1 = (( RAT_Sums A) + ( RAT_Sums B));

      set S2 = ( RAT_Sums (A \/ B));

      

       A4: S1 = { (a + b) where a,b be Point of X : a in D1 & b in D2 } by IDEAL_1:def 19;

      now

        let p be object;

        assume p in S1;

        then

        consider a,b be Point of X such that

         A5: p = (a + b) & a in D1 & b in D2 by A4;

        consider l1 be Linear_Combination of A such that

         A6: a = ( Sum l1) & ( rng l1) c= RAT by A5;

        consider l2 be Linear_Combination of B such that

         A7: b = ( Sum l2) & ( rng l2) c= RAT by A5;

        ex l be Linear_Combination of (A \/ B) st ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) & ( rng l) c= RAT & ( Sum l) = (( Sum l1) + ( Sum l2)) by A3, A6, A7, Th10;

        hence p in S2 by A5, A6, A7;

      end;

      then

       A8: S1 c= S2;

      now

        let p be object;

        assume p in S2;

        then

        consider l be Linear_Combination of (A \/ B) such that

         A9: p = ( Sum l) & ( rng l) c= RAT ;

        consider l1 be Linear_Combination of A, l2 be Linear_Combination of B such that

         A10: ( rng l1) c= RAT & ( rng l2) c= RAT & ( Sum l) = (( Sum l1) + ( Sum l2)) by A3, A9, Th11;

        ( Sum l1) in D1 & ( Sum l2) in D2 by A10;

        hence p in S1 by A4, A9, A10;

      end;

      then S2 c= S1;

      hence thesis by A8;

    end;

    

     Lm13: for X be RealLinearSpace holds ( RAT_Sums ( {} X)) is countable

    proof

      let X be RealLinearSpace;

      set A = ( {} X);

      set D = ( RAT_Sums A);

      now

        let x be object;

        hereby

          assume x in D;

          then

          consider l be Linear_Combination of A such that

           A3: x = ( Sum l) & ( rng l) c= RAT ;

          ( Carrier l) c= A by RLVECT_2:def 6;

          then ( Carrier l) = {} ;

          hence x = ( 0. X) by A3, RLVECT_2: 34;

        end;

        assume

         A4: x = ( 0. X);

        

         A5: ( ZeroLC X) is Linear_Combination of A by RLVECT_2: 22;

        

         A6: ( Sum ( ZeroLC X)) = ( 0. X) by RLVECT_2: 30;

        now

          let a be object;

          assume a in ( rng ( ZeroLC X));

          then ex x be Element of X st a = (( ZeroLC X) . x) by FUNCT_2: 113;

          then a = 0 by RLVECT_2: 20;

          hence a in RAT by RAT_1:def 2;

        end;

        then

         A7: ( rng ( ZeroLC X)) c= RAT ;

        thus x in D by A4, A5, A6, A7;

      end;

      then D = {( 0. X)} by TARSKI:def 1;

      hence D is countable;

    end;

    

     Th14: for X be RealLinearSpace, A be finite Subset of X holds ( RAT_Sums A) is countable

    proof

      let X be RealLinearSpace, A be finite Subset of X;

      set D = ( RAT_Sums A);

      defpred P[ Nat] means for B be finite Subset of X st ( card B) <= $1 holds ( RAT_Sums B) is countable;

       A2:

      now

        let B be finite Subset of X, E be set;

        assume ( card B) <= 0 ;

        then B = ( {} X);

        hence ( RAT_Sums B) is countable by Lm13;

      end;

      then

       A4: P[ 0 ];

      

       A5: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A6: P[k];

        hereby

          let B be finite Subset of X;

          assume

           A7: ( card B) <= (k + 1);

          set E = ( RAT_Sums B);

          per cases ;

            suppose ( card B) = 0 ;

            hence E is countable by A2;

          end;

            suppose ( card B) <> 0 ;

            then B <> {} ;

            then

            consider v be object such that

             A8: v in B by XBOOLE_0:def 1;

            reconsider v as Element of X by A8;

            

             A9: ((B \ {v}) \/ {v}) = B by A8, XBOOLE_1: 45, ZFMISC_1: 31;

            v in {v} by TARSKI:def 1;

            then not v in (B \ {v}) by XBOOLE_0:def 5;

            then

             A10: ( card ((B \ {v}) \/ {v})) = (( card (B \ {v})) + 1) by CARD_2: 41;

            set D1 = ( RAT_Sums (B \ {v}));

            set D2 = ( RAT_Sums {v});

            

             A11: E = (D1 + D2) by A9, Th12, XBOOLE_1: 79;

            D1 is countable & D2 is countable by A6, A7, A9, A10, Lm6, XREAL_1: 6;

            hence E is countable by A11, Th5;

          end;

        end;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A5);

      then P[( card A)];

      hence D is countable;

    end;

    registration

      let X be RealLinearSpace, A be finite Subset of X;

      cluster ( RAT_Sums A) -> countable;

      coherence by Th14;

    end

    theorem :: NORMSP_4:12

    

     Th15: for X be RealLinearSpace, x be sequence of X, A be finite Subset of X st A c= ( rng x) holds ex n be Nat st A c= ( rng (x | ( Segm n)))

    proof

      let X be RealLinearSpace, x be sequence of X;

      defpred P[ Nat] means for A be finite Subset of X st ( card A) = $1 & A c= ( rng x) holds ex n be Nat st A c= ( rng (x | ( Segm n)));

      

       A1: P[ 0 ]

      proof

        let A be finite Subset of the carrier of X;

        assume

         A2: ( card A) = 0 & A c= ( rng x);

        set n = the Nat;

        take n;

        thus A c= ( rng (x | ( Segm n))) by A2;

      end;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: P[k];

        let A be finite Subset of the carrier of X;

        assume

         A5: ( card A) = (k + 1) & A c= ( rng x);

        then A <> {} ;

        then

        consider w be object such that

         A6: w in A by XBOOLE_0:def 1;

        reconsider w as Element of the carrier of X by A6;

        

         A7: ( card (A \ {w})) = (( card A) - ( card {w})) by A6, CARD_2: 44, ZFMISC_1: 31

        .= ((k + 1) - 1) by A5, CARD_2: 42;

        reconsider A0 = (A \ {w}) as finite Subset of X;

        A0 c= A by XBOOLE_1: 36;

        then A0 c= ( rng x) by A5;

        then

        consider n0 be Nat such that

         A8: A0 c= ( rng (x | ( Segm n0))) by A4, A7;

        consider n1 be object such that

         A9: n1 in NAT & w = (x . n1) by A5, A6, FUNCT_2: 11;

        reconsider n1 as Nat by A9;

        set n = ((n0 + n1) + 1);

        take n;

        

         A10: A = (A0 \/ {w}) by A6, XBOOLE_1: 45, ZFMISC_1: 31;

        n0 < n by NAT_1: 11, NAT_1: 13;

        then (x | ( Segm n0)) c= (x | ( Segm n)) by NAT_1: 39, RELAT_1: 75;

        then ( rng (x | ( Segm n0))) c= ( rng (x | ( Segm n))) by RELAT_1: 11;

        then

         A11: A0 c= ( rng (x | ( Segm n))) by A8;

        n1 < n by NAT_1: 11, NAT_1: 13;

        then n1 in ( Segm n) & ( dom x) = NAT by FUNCT_2:def 1, NAT_1: 44;

        then {w} c= ( rng (x | ( Segm n))) by A9, FUNCT_1: 50, ZFMISC_1: 31;

        hence A c= ( rng (x | ( Segm n))) by A10, A11, XBOOLE_1: 8;

      end;

      

       A12: for k be Nat holds P[k] from NAT_1:sch 2( A1, A3);

      let A be finite Subset of the carrier of X;

      assume

       A13: A c= ( rng x);

      ( card A) is Nat;

      hence ex n be Nat st A c= ( rng (x | ( Segm n))) by A12, A13;

    end;

    

     Th16: for X be RealLinearSpace, x be sequence of X holds ( RAT_Sums ( rng x)) is countable

    proof

      let X be RealLinearSpace, x be sequence of X;

      set D = ( RAT_Sums ( rng x));

      defpred P[ Nat, object] means $2 = ( RAT_Sums ( rng (x | ( Segm $1))));

      

       A2: for n be Element of NAT holds ex X1 be Element of ( bool the carrier of X) st P[n, X1];

      consider E be Function of NAT , ( bool the carrier of X) such that

       A3: for n be Element of NAT holds P[n, (E . n)] from FUNCT_2:sch 3( A2);

      for z be object st z in ( RAT_Sums ( rng x)) holds z in ( Union E)

      proof

        let z be object;

        assume z in ( RAT_Sums ( rng x));

        then

        consider l be Linear_Combination of ( rng x) such that

         A4: z = ( Sum l) & ( rng l) c= RAT ;

        consider nmax be Nat such that

         A5: ( Carrier l) c= ( rng (x | ( Segm nmax))) by RLVECT_2:def 6, Th15;

        reconsider nmax as Element of NAT by ORDINAL1:def 12;

        

         A6: (E . nmax) = ( RAT_Sums ( rng (x | ( Segm nmax)))) by A3;

        l is Linear_Combination of ( rng (x | nmax)) by A5, RLVECT_2:def 6;

        then

         A7: z in (E . nmax) by A4, A6;

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

        hence z in ( Union E) by A7, CARD_5: 2;

      end;

      then

       A8: ( RAT_Sums ( rng x)) c= ( Union E);

      for n be set st n in ( dom E) holds (E . n) is countable

      proof

        let n be set;

        assume n in ( dom E);

        then

        reconsider n1 = n as Element of NAT ;

        (E . n) = ( RAT_Sums ( rng (x | ( Segm n1)))) by A3;

        hence (E . n) is countable;

      end;

      then ( Union E) is countable by CARD_4: 11;

      hence D is countable by A8;

    end;

    registration

      let X be RealLinearSpace, x be sequence of X;

      cluster ( RAT_Sums ( rng x)) -> countable;

      coherence by Th16;

    end

    theorem :: NORMSP_4:13

    

     Th17: for X be RealNormSpace, x be sequence of X holds ( RAT_Sums ( rng x)) is Subset of the carrier of ( NLin ( rng x))

    proof

      let X be RealNormSpace, x be sequence of X;

      set D = ( RAT_Sums ( rng x));

      for z be object st z in D holds z in the carrier of ( NLin ( rng x))

      proof

        let z be object;

        assume z in D;

        then

        consider l be Linear_Combination of ( rng x) such that

         A2: z = ( Sum l) & ( rng l) c= RAT ;

        z in ( Lin ( rng x)) by A2, RLVECT_3: 14;

        hence z in the carrier of ( NLin ( rng x));

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: NORMSP_4:14

    

     Th18: for X be RealNormSpace, Y be Subset of X holds the carrier of ( NLin Y) c= the carrier of ( ClNLin Y) & ex Z be Subset of X st Z = the carrier of ( NLin Y) & ( Cl Z) = the carrier of ( ClNLin Y)

    proof

      let X be RealNormSpace, Y be Subset of X;

      ex Z be Subset of X st Z = the carrier of ( Lin Y) & ( ClNLin Y) = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),X)), ( Add_ (( Cl Z),X)), ( Mult_ (( Cl Z),X)), ( Norm_ (( Cl Z),X)) #) by NORMSP_3:def 20;

      hence thesis by NORMSP_3: 4;

    end;

    theorem :: NORMSP_4:15

    

     Th19: for X be RealNormSpace, x be sequence of X holds ( RAT_Sums ( rng x)) is countable Subset of the carrier of ( ClNLin ( rng x))

    proof

      let X be RealNormSpace, x be sequence of X;

      set D = ( RAT_Sums ( rng x));

      

       A1: D is Subset of the carrier of ( NLin ( rng x)) by Th17;

      the carrier of ( NLin ( rng x)) c= the carrier of ( ClNLin ( rng x)) by Th18;

      hence thesis by A1, XBOOLE_1: 1;

    end;

    theorem :: NORMSP_4:16

    

     Th21: for z,e be Real st 0 < e holds ex q be Element of RAT st q <> 0 & |.(z - q).| < e

    proof

      let z be Real, e be Real;

      assume

       A1: 0 < e;

      then ( 0 + z) < (z + e) by XREAL_1: 8;

      then

      consider p1,p2 be Rational such that

       A2: z < p1 & p1 < p2 & p2 < (z + e) by BORSUK_5: 26;

      per cases ;

        suppose

         A3: 0 <= z;

        p1 < (z + e) by A2, XXREAL_0: 2;

        then (p1 - z) < ((z + e) - z) by XREAL_1: 14;

        then

         A4: |.(p1 - z).| < e by ABSVALUE:def 1, A2, XREAL_1: 48;

        reconsider p1 as Element of RAT by RAT_1:def 2;

        take p1;

        thus p1 <> 0 by A2, A3;

        thus |.(z - p1).| < e by A4, COMPLEX1: 60;

      end;

        suppose

         A5: z < 0 ;

        (z - e) < (z - 0 ) by A1, XREAL_1: 15;

        then

        consider p1,p2 be Rational such that

         A6: (z - e) < p1 & p1 < p2 & p2 < z by BORSUK_5: 26;

        ((z - e) - z) < (p1 - z) by A6, XREAL_1: 14;

        then

         A7: ( 0 - (p1 - z)) < ( 0 - ( - e)) by XREAL_1: 15;

        

         A8: p1 < z by A6, XXREAL_0: 2;

        reconsider p1 as Element of RAT by RAT_1:def 2;

        take p1;

        thus p1 <> 0 by A5, A6;

        thus |.(z - p1).| < e by A7, A8, ABSVALUE:def 1, XREAL_1: 48;

      end;

    end;

    theorem :: NORMSP_4:17

    

     Th22: for X be RealNormSpace, w be Point of X, e be Real, l be Linear_Combination of {w} st 0 < e holds ex m be Linear_Combination of {w} st ( Carrier m) = ( Carrier l) & ( rng m) c= RAT & ||.(( Sum l) - ( Sum m)).|| < e

    proof

      let X be RealNormSpace, w be Point of X, e be Real, l be Linear_Combination of {w};

      assume

       A1: 0 < e;

      

       A2: ( Carrier l) c= {w} by RLVECT_2:def 6;

      per cases ;

        suppose

         A3: not w in ( Carrier l);

        set m = l;

        take m;

        thus ( Carrier m) = ( Carrier l);

        for y be object st y in ( rng m) holds y in RAT

        proof

          let y be object;

          assume y in ( rng m);

          then

          consider x be object such that

           A4: x in ( dom m) & y = (m . x) by FUNCT_1:def 3;

          reconsider x as Point of X by A4;

           not x in ( Carrier l) by A2, A3, TARSKI:def 1;

          then y is integer by A4;

          hence y in RAT by NUMBERS: 14;

        end;

        hence ( rng m) c= RAT ;

        (( Sum l) - ( Sum m)) = ( 0. X) by RLVECT_1: 15;

        hence ||.(( Sum l) - ( Sum m)).|| < e by A1;

      end;

        suppose

         A5: w in ( Carrier l);

        then

         A6: ( Carrier l) = {w} & (l . w) <> 0 by RLVECT_2: 19, RLVECT_2:def 6, ZFMISC_1: 31;

        per cases ;

          suppose

           A7: w = ( 0. X);

          

           A8: ( Sum l) = ((l . w) * w) by RLVECT_2: 32;

          set m = ((1 / (l . w)) * l);

          ( Carrier m) = ( Carrier l) by A6, RLVECT_2: 42;

          then

          reconsider m as Linear_Combination of {w} by RLVECT_2:def 6;

          take m;

          thus ( Carrier m) = ( Carrier l) by A6, RLVECT_2: 42;

          for y be object st y in ( rng m) holds y in RAT

          proof

            let y be object;

            assume y in ( rng m);

            then

            consider x be object such that

             A9: x in ( dom m) & y = (m . x) by FUNCT_1:def 3;

            reconsider x as Point of X by A9;

            per cases ;

              suppose not x in ( Carrier l);

              then

               A10: (l . x) = 0 ;

              y = ((1 / (l . w)) * (l . x)) by A9, RLVECT_2:def 11;

              then y is integer by A10;

              hence y in RAT by NUMBERS: 14;

            end;

              suppose x in ( Carrier l);

              then x = w by A6, TARSKI:def 1;

              then y = ((1 / (l . w)) * (l . w)) by A9, RLVECT_2:def 11;

              then y is integer by A5, RLVECT_2: 19, XCMPLX_1: 87;

              hence y in RAT by NUMBERS: 14;

            end;

          end;

          hence ( rng m) c= RAT ;

          ( Sum m) = ((1 / (l . w)) * ( Sum l)) by RLVECT_3: 2;

          hence ||.(( Sum l) - ( Sum m)).|| < e by A1, A7, A8;

        end;

          suppose

           A11: w <> ( 0. X);

          then

           A12: ||.w.|| <> 0 by NORMSP_0:def 5;

          then

          consider q be Element of RAT such that

           A13: q <> 0 & |.((l . w) - q).| < (e / ||.w.||) by A1, Th21;

          set m = ((q / (l . w)) * l);

          ( Carrier m) = ( Carrier l) by A6, A13, RLVECT_2: 42;

          then

          reconsider m as Linear_Combination of {w} by RLVECT_2:def 6;

          take m;

          thus ( Carrier m) = ( Carrier l) by A6, A13, RLVECT_2: 42;

          for y be object st y in ( rng m) holds y in RAT

          proof

            let y be object;

            assume y in ( rng m);

            then

            consider x be object such that

             A14: x in ( dom m) & y = (m . x) by FUNCT_1:def 3;

            reconsider x as Point of X by A14;

            per cases ;

              suppose not x in ( Carrier l);

              then

               A15: (l . x) = 0 ;

              y = ((q / (l . w)) * (l . x)) by A14, RLVECT_2:def 11;

              then y is integer by A15;

              hence y in RAT by NUMBERS: 14;

            end;

              suppose x in ( Carrier l);

              then x = w by A6, TARSKI:def 1;

              then y = ((q / (l . w)) * (l . w)) by A14, RLVECT_2:def 11;

              then y = q by A5, RLVECT_2: 19, XCMPLX_1: 87;

              hence y in RAT ;

            end;

          end;

          hence ( rng m) c= RAT ;

          

           A16: ( Sum m) = ((q / (l . w)) * ( Sum l)) by RLVECT_3: 2

          .= ((q / (l . w)) * ((l . w) * w)) by RLVECT_2: 32

          .= (((q / (l . w)) * (l . w)) * w) by RLVECT_1:def 7

          .= (q * w) by A5, RLVECT_2: 19, XCMPLX_1: 87;

          (( Sum l) - ( Sum m)) = (((l . w) * w) - ( Sum m)) by RLVECT_2: 32

          .= (((l . w) - q) * w) by A16, RLVECT_1: 35;

          then

           A17: ||.(( Sum l) - ( Sum m)).|| = ( |.((l . w) - q).| * ||.w.||) by NORMSP_1:def 1;

          ( |.((l . w) - q).| * ||.w.||) < ((e / ||.w.||) * ||.w.||) by A12, A13, XREAL_1: 68;

          hence ||.(( Sum l) - ( Sum m)).|| < e by A11, A17, NORMSP_0:def 5, XCMPLX_1: 87;

        end;

      end;

    end;

    theorem :: NORMSP_4:18

    

     Th23: for X be RealNormSpace, A be Subset of X, e be Real, l be Linear_Combination of A st 0 < e holds ex m be Linear_Combination of A st ( Carrier m) = ( Carrier l) & ( rng m) c= RAT & ||.(( Sum l) - ( Sum m)).|| < e

    proof

      let X be RealNormSpace, A be Subset of X;

      defpred P[ Nat] means for e be Real, l be Linear_Combination of A st 0 < e & ( card ( Carrier l)) = $1 holds ex m be Linear_Combination of A st ( Carrier m) = ( Carrier l) & ( rng m) c= RAT & ||.(( Sum l) - ( Sum m)).|| < e;

      

       A1: P[ 0 ]

      proof

        let e be Real, l be Linear_Combination of A;

        assume

         A2: 0 < e & ( card ( Carrier l)) = 0 ;

        then ( Carrier l) = {} ;

        then

         A3: ( Sum l) = ( 0. X) by RLVECT_2: 34;

        reconsider a = 1 as Real;

        reconsider m = (a * l) as Linear_Combination of A by RLVECT_2: 44;

        take m;

        thus ( Carrier m) = ( Carrier l) by RLVECT_2: 42;

        for y be object st y in ( rng m) holds y in RAT

        proof

          let y be object;

          assume y in ( rng m);

          then

          consider x be object such that

           A4: x in ( dom m) & y = (m . x) by FUNCT_1:def 3;

          reconsider x as Point of X by A4;

          

           A5: not x in ( Carrier l) by A2;

          y = (a * (l . x)) by A4, RLVECT_2:def 11;

          then y is integer by A5;

          hence y in RAT by NUMBERS: 14;

        end;

        hence ( rng m) c= RAT ;

        ( Sum m) = (a * ( Sum l)) by RLVECT_3: 2;

        hence ||.(( Sum l) - ( Sum m)).|| < e by A2, A3;

      end;

      

       A6: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A7: P[k];

        let e be Real, l be Linear_Combination of A;

        assume

         A8: 0 < e & ( card ( Carrier l)) = (k + 1);

        then ( Carrier l) <> {} ;

        then

        consider w be object such that

         A9: w in ( Carrier l) by XBOOLE_0:def 1;

        reconsider w as Element of the carrier of X by A9;

        

         A10: ( card (( Carrier l) \ {w})) = (( card ( Carrier l)) - ( card {w})) by A9, CARD_2: 44, ZFMISC_1: 31

        .= ((k + 1) - 1) by A8, CARD_2: 42;

        reconsider A0 = (( Carrier l) \ {w}) as finite Subset of X;

        reconsider B0 = {w} as finite Subset of X;

        (A0 \/ B0) = (( Carrier l) \/ B0) by XBOOLE_1: 39;

        then (A0 \/ B0) = ( Carrier l) by A9, XBOOLE_1: 12, ZFMISC_1: 31;

        then

         A11: l is Linear_Combination of (A0 \/ B0) by RLVECT_2:def 6;

        consider l1 be Linear_Combination of A0, l2 be Linear_Combination of B0 such that

         A13: ( Carrier l) = (( Carrier l1) \/ ( Carrier l2)) & l = (l1 + l2) & ( Carrier l1) = (( Carrier l) \ B0) & ( Carrier l2) = (( Carrier l) \ A0) by A11, Th9, XBOOLE_1: 79;

        

         A14: ( Carrier l) c= A by RLVECT_2:def 6;

        ( Carrier l1) c= ( Carrier l) by A13, XBOOLE_1: 36;

        then ( Carrier l1) c= A by A14;

        then l1 is Linear_Combination of A by RLVECT_2:def 6;

        then

        consider m1 be Linear_Combination of A such that

         A15: ( Carrier m1) = ( Carrier l1) & ( rng m1) c= RAT & ||.(( Sum l1) - ( Sum m1)).|| < (e / 2) by A7, A8, A10, A13;

        

         A16: m1 is Linear_Combination of A0 by A15, RLVECT_2:def 6;

        consider m2 be Linear_Combination of {w} such that

         A17: ( Carrier m2) = ( Carrier l2) & ( rng m2) c= RAT & ||.(( Sum l2) - ( Sum m2)).|| < (e / 2) by A8, Th22;

        consider m be Linear_Combination of (A0 \/ {w}) such that

         A18: ( Carrier m) = (( Carrier m1) \/ ( Carrier m2)) & ( rng m) c= RAT & ( Sum m) = (( Sum m1) + ( Sum m2)) by XBOOLE_1: 79, A15, A16, A17, Th10;

        

         A19: m is Linear_Combination of A by A13, A15, A17, A18, RLVECT_2:def 6;

        (( Sum l) - ( Sum m)) = ((( Sum l1) + ( Sum l2)) - ( Sum m)) by A13, RLVECT_3: 1

        .= (((( Sum l1) + ( Sum l2)) - ( Sum m1)) - ( Sum m2)) by A18, RLVECT_1: 27

        .= ((( Sum l2) + (( Sum l1) - ( Sum m1))) - ( Sum m2)) by RLVECT_1: 28

        .= ((( Sum l1) - ( Sum m1)) + (( Sum l2) - ( Sum m2))) by RLVECT_1: 28;

        then

         A20: ||.(( Sum l) - ( Sum m)).|| <= ( ||.(( Sum l1) - ( Sum m1)).|| + ||.(( Sum l2) - ( Sum m2)).||) by NORMSP_1:def 1;

        ( ||.(( Sum l1) - ( Sum m1)).|| + ||.(( Sum l2) - ( Sum m2)).||) < ((e / 2) + (e / 2)) by A15, A17, XREAL_1: 8;

        then ||.(( Sum l) - ( Sum m)).|| < e by A20, XXREAL_0: 2;

        hence thesis by A13, A15, A17, A18, A19;

      end;

      

       A21: for k be Nat holds P[k] from NAT_1:sch 2( A1, A6);

      let e be Real, l be Linear_Combination of A;

      assume

       A22: 0 < e;

      ( card ( Carrier l)) is Nat;

      hence thesis by A21, A22;

    end;

    

     Th24: for X be RealNormSpace, x be sequence of X, D be Subset of the carrier of ( NLin ( rng x)) st D = ( RAT_Sums ( rng x)) holds D is dense

    proof

      let X be RealNormSpace, x be sequence of X, D be Subset of the carrier of ( NLin ( rng x));

      assume

       A1: D = ( RAT_Sums ( rng x));

      for S be Subset of ( NLin ( rng x)) st S <> {} & S is open holds D meets S

      proof

        let S be Subset of ( NLin ( rng x));

        assume

         A2: S <> {} & S is open;

        consider z be object such that

         A3: z in S by A2, XBOOLE_0:def 1;

        reconsider z as Point of ( NLin ( rng x)) by A3;

        consider e be Real such that

         A4: 0 < e & { y where y be Point of ( NLin ( rng x)) : ||.(y - z).|| < e } c= S by A2, A3, NDIFF_1: 3;

        z in ( Lin ( rng x));

        then

        consider l be Linear_Combination of ( rng x) such that

         A5: z = ( Sum l) by RLVECT_3: 14;

        consider m be Linear_Combination of ( rng x) such that

         A6: ( Carrier m) = ( Carrier l) & ( rng m) c= RAT & ||.(( Sum l) - ( Sum m)).|| < e by A4, Th23;

        ( Sum m) in ( Lin ( rng x)) by RLVECT_3: 14;

        then

        reconsider y = ( Sum m) as Point of ( NLin ( rng x));

        ( - ( Sum m)) = (( - 1) * ( Sum m)) by RLVECT_1: 16

        .= (( - 1) * y) by NORMSP_3: 28

        .= ( - y) by RLVECT_1: 16;

        then (( Sum l) - ( Sum m)) = (z - y) by A5, NORMSP_3: 28;

        then ||.(( Sum l) - ( Sum m)).|| = ||.(z - y).|| by NORMSP_3: 28;

        then ||.(y - z).|| < e by A6, NORMSP_1: 7;

        then

         A8: y in { v where v be Point of ( NLin ( rng x)) : ||.(v - z).|| < e };

        y in D by A1, A6;

        hence D meets S by A4, A8, XBOOLE_0:def 4;

      end;

      hence thesis by NORMSP_3: 17;

    end;

    theorem :: NORMSP_4:19

    for X be RealNormSpace, x be sequence of X holds ( RAT_Sums ( rng x)) is dense Subset of the carrier of ( NLin ( rng x)) by Th17, Th24;

    

     Th25: for X be RealNormSpace, x be sequence of X, D be Subset of the carrier of ( ClNLin ( rng x)) st D = ( RAT_Sums ( rng x)) holds D is dense

    proof

      let X be RealNormSpace, x be sequence of X, D be Subset of the carrier of ( ClNLin ( rng x));

      assume

       A1: D = ( RAT_Sums ( rng x));

      then

      reconsider D0 = D as Subset of the carrier of ( NLin ( rng x)) by Th17;

      

       A2: D0 is dense by A1, Th24;

      ex Z be Subset of X st Z = the carrier of ( NLin ( rng x)) & ( Cl Z) = the carrier of ( ClNLin ( rng x)) by Th18;

      hence D is dense by A2, Th3;

    end;

    theorem :: NORMSP_4:20

    for X be RealNormSpace, x be sequence of X holds ( RAT_Sums ( rng x)) is dense Subset of the carrier of ( ClNLin ( rng x)) by Th19, Th25;

    theorem :: NORMSP_4:21

    

     Th26: for X be RealNormSpace st ex D be Subset of the carrier of X st D is dense countable holds X is separable

    proof

      let X be RealNormSpace;

      set Y = ( LinearTopSpaceNorm X);

      given D0 be Subset of the carrier of X such that

       A1: D0 is dense countable;

      reconsider D = D0 as Subset of Y by NORMSP_2:def 4;

      D is dense by A1, NORMSP_3: 15;

      then

       A2: ( density Y) c= ( card D) by TOPGEN_1:def 12;

      ( card D) c= omega by A1;

      then ( density Y) c= omega by A2;

      hence thesis by TOPGEN_1:def 13;

    end;

    begin

    registration

      let X be RealNormSpace, x be sequence of X;

      cluster ( ClNLin ( rng x)) -> separable;

      coherence

      proof

        ( RAT_Sums ( rng x)) is countable Subset of the carrier of ( ClNLin ( rng x)) by Th19;

        hence ( ClNLin ( rng x)) is separable by Th25, Th26;

      end;

    end

    theorem :: NORMSP_4:22

    for X be RealNormSpace, Y be SubRealNormSpace of X, L be Lipschitzian linear-Functional of X holds (L | the carrier of Y) is Lipschitzian linear-Functional of Y

    proof

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

      set Y1 = the carrier of Y;

      

       A1: the carrier of Y c= the carrier of X by DUALSP01:def 16;

      then

      reconsider L1 = (L | Y1) as Functional of Y by FUNCT_2: 32;

      

       A2: L1 is additive

      proof

        let x,y be Point of Y;

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

        

        thus (L1 . (x + y)) = (L . (x + y)) by FUNCT_1: 49

        .= (L . (x1 + y1)) by NORMSP_3: 28

        .= ((L . x1) + (L . y1)) by HAHNBAN:def 2

        .= ((L1 . x) + (L . y)) by FUNCT_1: 49

        .= ((L1 . x) + (L1 . y)) by FUNCT_1: 49;

      end;

      

       A3: L1 is homogeneous

      proof

        let x be Point of Y, r be Real;

        reconsider x1 = x as Point of X by A1;

        

        thus (L1 . (r * x)) = (L . (r * x)) by FUNCT_1: 49

        .= (L . (r * x1)) by NORMSP_3: 28

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

        .= (r * (L1 . x)) by FUNCT_1: 49;

      end;

      consider K be Real such that

       A4: 0 <= K & for x be Point of X holds |.(L . x).| <= (K * ||.x.||) by DUALSP01:def 9;

      for x be Point of Y holds |.(L1 . x).| <= (K * ||.x.||)

      proof

        let x be Point of Y;

        reconsider x1 = x as Point of X by A1;

         |.(L . x1).| <= (K * ||.x1.||) by A4;

        then |.(L . x1).| <= (K * ||.x.||) by NORMSP_3: 28;

        hence thesis by FUNCT_1: 49;

      end;

      then L1 is Lipschitzian by A4;

      hence thesis by A2, A3;

    end;

    

     Th29: for X,Y be RealNormSpace, A be Subset of X, B be Subset of Y, L be Lipschitzian LinearOperator of X, Y st L is isomorphism & B = (L .: A) & A is dense holds B is dense

    proof

      let X,Y be RealNormSpace, A be Subset of X, B be Subset of Y, L be Lipschitzian LinearOperator of X, Y;

      assume

       A1: L is isomorphism & B = (L .: A) & A is dense;

      for y be Point of Y holds ex seq be sequence of Y st ( rng seq) c= B & seq is convergent & ( lim seq) = y

      proof

        let y be Point of Y;

        y in the carrier of Y;

        then y in ( rng L) by A1, FUNCT_2:def 3;

        then

        consider x be Point of X such that

         A2: y = (L . x) by FUNCT_2: 113;

        consider seq be sequence of X such that

         A3: ( rng seq) c= A & seq is convergent & ( lim seq) = x by A1, NORMSP_3: 14;

        reconsider seq1 = (L * seq) as sequence of Y;

        (L .: ( rng seq)) c= (L .: A) by A3, RELAT_1: 123;

        then

         A4: ( rng seq1) c= B by A1, RELAT_1: 127;

        seq1 is convergent & ( lim seq1) = (L . ( lim seq)) by A3, NORMSP_3: 38;

        hence thesis by A2, A3, A4;

      end;

      hence B is dense by NORMSP_3: 14;

    end;

    theorem :: NORMSP_4:23

    

     Th30: for X,Y be RealNormSpace, A be Subset of X, B be Subset of Y, L be Lipschitzian LinearOperator of X, Y st L is isomorphism & B = (L .: A) holds A is dense iff B is dense

    proof

      let X,Y be RealNormSpace, A be Subset of X, B be Subset of Y, L be Lipschitzian LinearOperator of X, Y;

      assume

       A1: L is isomorphism & B = (L .: A);

      then

      consider K be Lipschitzian LinearOperator of Y, X such that

       A2: K = (L " ) & K is isomorphism by NORMSP_3: 37;

      thus A is dense implies B is dense by A1, Th29;

      assume

       A3: B is dense;

      A c= the carrier of X;

      then A c= ( dom L) by FUNCT_2:def 1;

      then (K .: B) = A by A1, A2, FUNCT_1: 107;

      hence A is dense by A2, A3, Th29;

    end;

    theorem :: NORMSP_4:24

    

     Th31: for X,Y be RealNormSpace st ex L be Lipschitzian LinearOperator of X, Y st L is isomorphism holds X is separable iff Y is separable

    proof

      let X,Y be RealNormSpace;

      given L be Lipschitzian LinearOperator of X, Y such that

       A1: L is isomorphism;

      consider K be Lipschitzian LinearOperator of Y, X such that

       A2: K = (L " ) & K is isomorphism by A1, NORMSP_3: 37;

      hereby

        assume X is separable;

        then

        consider seq be sequence of X such that

         A3: ( rng seq) is dense by NORMSP_3: 21;

        reconsider seq1 = (L * seq) as sequence of Y;

        ( rng seq1) = (L .: ( rng seq)) by RELAT_1: 127;

        then ( rng seq1) is dense by A1, A3, Th30;

        hence Y is separable by NORMSP_3: 21;

      end;

      assume Y is separable;

      then

      consider seq be sequence of Y such that

       A4: ( rng seq) is dense by NORMSP_3: 21;

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

      ( rng seq1) = (K .: ( rng seq)) by RELAT_1: 127;

      then ( rng seq1) is dense by A2, A4, Th30;

      hence X is separable by NORMSP_3: 21;

    end;

    theorem :: NORMSP_4:25

    for X be RealNormSpace st X is non trivial & X is Reflexive holds X is separable iff ( DualSp ( DualSp X)) is separable

    proof

      let X be RealNormSpace;

      assume

       A1: X is non trivial & X is Reflexive;

      then

      consider DuX be SubRealNormSpace of ( DualSp ( DualSp X)), L be Lipschitzian LinearOperator of X, DuX such that

       A2: L is bijective & DuX = ( Im ( BidualFunc X)) & (for x be Point of X holds (L . x) = ( BiDual x)) & for x be Point of X holds ||.x.|| = ||.(L . x).|| by DUALSP02: 10;

      

       A3: ( Im ( BidualFunc X)) = ( DualSp ( DualSp X)) by A1, DUALSP02: 22;

      then

      reconsider L as Lipschitzian LinearOperator of X, ( DualSp ( DualSp X)) by A2;

      L is isomorphism by A2, A3;

      hence thesis by Th31;

    end;

    begin

    theorem :: NORMSP_4:26

    for X be RealNormSpace, Y,Z be Subset of X st Z = the carrier of ( Lin Y) holds the carrier of ( Lin Z) = Z by RLVECT_3: 18;

    theorem :: NORMSP_4:27

    

     Th35: for X be RealBanachSpace, Y be Subset of X holds ex Z be Subset of X st Z = the carrier of ( Lin Y) & ( ClNLin Y) = ( NLin ( Cl Z)) & ( Cl Z) is linearly-closed & ( Cl Z) <> {}

    proof

      let X be RealBanachSpace, Y be Subset of X;

      consider Z be Subset of X such that

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

      

       A2: the carrier of ( Lin ( Cl Z)) = ( Cl Z) by A1, NORMSP_3: 13, NORMSP_3: 31;

      

       A3: ( NLin ( Cl Z)) = NORMSTR (# the carrier of ( Lin ( Cl Z)), ( 0. ( Lin ( Cl Z))), the addF of ( Lin ( Cl Z)), the Mult of ( Lin ( Cl Z)), ( Norm_ (the carrier of ( Lin ( Cl Z)),X)) #);

      

       A4: ( Zero_ (( Cl Z),X)) = ( 0. X) by A1, NORMSP_3: 13, RSSPACE:def 10

      .= ( 0. ( Lin ( Cl Z))) by RLSUB_1:def 2;

      

       A5: ( Add_ (( Cl Z),X)) = (the addF of X || ( Cl Z)) by A1, NORMSP_3: 13, RSSPACE:def 8

      .= the addF of ( Lin ( Cl Z)) by A2, RLSUB_1:def 2;

      

       A6: ( Mult_ (( Cl Z),X)) = (the Mult of X | [: REAL , ( Cl Z):]) by A1, NORMSP_3: 13, RSSPACE:def 9

      .= the Mult of ( Lin ( Cl Z)) by A2, RLSUB_1:def 2;

      ( Norm_ (( Cl Z),X)) = ( Norm_ (the carrier of ( Lin ( Cl Z)),X)) by A1, NORMSP_3: 13, NORMSP_3: 31;

      hence thesis by A1, A3, A4, A5, A6, NORMSP_3: 13;

    end;

    theorem :: NORMSP_4:28

    for X be RealBanachSpace, Y be Subset of X holds ( ClNLin Y) is RealBanachSpace

    proof

      let X be RealBanachSpace, Y be Subset of X;

      ex Z be Subset of X st Z = the carrier of ( Lin Y) & ( ClNLin Y) = ( NLin ( Cl Z)) & ( Cl Z) is linearly-closed & ( Cl Z) <> {} by Th35;

      hence thesis by NORMSP_3: 49;

    end;

    theorem :: NORMSP_4:29

    for X be RealBanachSpace, Y be Subset of X st X is Reflexive holds ( ClNLin Y) is Reflexive

    proof

      let X be RealBanachSpace, Y be Subset of X;

      assume

       A1: X is Reflexive;

      ex Z be Subset of X st Z = the carrier of ( Lin Y) & ( ClNLin Y) = ( NLin ( Cl Z)) & ( Cl Z) is linearly-closed & ( Cl Z) <> {} by Th35;

      hence thesis by A1, DUALSP02: 24;

    end;