normsp_3.miz



    begin

    registration

      let X be RealNormSpace;

      cluster open closed for Subset of X;

      correctness

      proof

        set F = the open closed Subset of ( LinearTopSpaceNorm X);

        reconsider G = F as Subset of X by NORMSP_2:def 4;

        take G;

        thus thesis by NORMSP_2: 32, NORMSP_2: 33;

      end;

    end

    theorem :: NORMSP_3:1

    for X be RealNormSpace, R be Subset of X holds R is closed iff (R ` ) is open;

    registration

      let X be RealNormSpace, R be closed Subset of X;

      cluster (R ` ) -> open;

      correctness ;

    end

    theorem :: NORMSP_3:2

    

     Th0: for X be RealNormSpace, R be Subset of X holds R is open iff (R ` ) is closed;

    registration

      let X be RealNormSpace, R be open Subset of X;

      cluster (R ` ) -> closed;

      correctness by Th0;

    end

    registration

      let X be RealNormSpace;

      cluster ( [#] X) -> closed;

      correctness ;

      cluster ( {} X) -> closed;

      correctness ;

      cluster ( [#] X) -> open;

      correctness

      proof

        ( [#] X) = ( [#] ( LinearTopSpaceNorm X)) by NORMSP_2:def 4;

        hence thesis by NORMSP_2: 33;

      end;

      cluster ( {} X) -> open;

      correctness

      proof

        ( [#] X) = ( [#] ( LinearTopSpaceNorm X)) by NORMSP_2:def 4;

        hence thesis by NORMSP_2: 33;

      end;

    end

    registration

      let X be RealNormSpace;

      let P,Q be closed Subset of X;

      cluster (P /\ Q) -> closed;

      correctness

      proof

        reconsider P1 = P, Q1 = Q as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        P1 is closed & Q1 is closed by NORMSP_2: 32;

        then (P1 /\ Q1) is closed;

        hence thesis by NORMSP_2: 32;

      end;

      cluster (P \/ Q) -> closed;

      correctness

      proof

        reconsider P1 = P, Q1 = Q as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        P1 is closed & Q1 is closed by NORMSP_2: 32;

        then (P1 \/ Q1) is closed;

        hence thesis by NORMSP_2: 32;

      end;

    end

    registration

      let X be RealNormSpace;

      let P,Q be open Subset of X;

      cluster (P /\ Q) -> open;

      correctness

      proof

        reconsider P1 = P, Q1 = Q as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        P1 is open & Q1 is open by NORMSP_2: 33;

        then (P1 /\ Q1) is open;

        hence thesis by NORMSP_2: 33;

      end;

      cluster (P \/ Q) -> open;

      correctness

      proof

        reconsider P1 = P, Q1 = Q as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        P1 is open & Q1 is open by NORMSP_2: 33;

        then (P1 \/ Q1) is open;

        hence thesis by NORMSP_2: 33;

      end;

    end

    definition

      let X be RealNormSpace, Y be Subset of X;

      :: NORMSP_3:def1

      func Cl Y -> Subset of X means

      : defcl: ex Z be Subset of ( LinearTopSpaceNorm X) st Z = Y & it = ( Cl Z);

      correctness

      proof

        reconsider Z = Y as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        ( Cl Z) is Subset of X by NORMSP_2:def 4;

        hence thesis;

      end;

    end

    registration

      let X be RealNormSpace, Y be Subset of X;

      cluster ( Cl Y) -> closed;

      correctness

      proof

        ex Z be Subset of ( LinearTopSpaceNorm X) st Z = Y & ( Cl Y) = ( Cl Z) by defcl;

        hence thesis by NORMSP_2: 32;

      end;

    end

    theorem :: NORMSP_3:3

    

     EQCL1: for X be RealNormSpace, Y be Subset of X, Z be Subset of ( LinearTopSpaceNorm X) st Y = Z holds ( Cl Y) = ( Cl Z)

    proof

      let X be RealNormSpace, Y be Subset of X, Z be Subset of ( LinearTopSpaceNorm X);

      assume

       A1: Y = Z;

      ex Z0 be Subset of ( LinearTopSpaceNorm X) st Z0 = Y & ( Cl Y) = ( Cl Z0) by defcl;

      hence ( Cl Y) = ( Cl Z) by A1;

    end;

    theorem :: NORMSP_3:4

    

     PRETOPC18: for X be RealNormSpace, Z be Subset of X holds Z c= ( Cl Z)

    proof

      let X be RealNormSpace, Z be Subset of X;

      reconsider W = Z as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      ( Cl Z) = ( Cl W) by EQCL1;

      hence Z c= ( Cl Z) by PRE_TOPC: 18;

    end;

    theorem :: NORMSP_3:5

    for X be RealNormSpace, Y be Subset of X, v be object st v in the carrier of X holds v in ( Cl Y) iff for G be Subset of X st G is open & v in G holds G meets Y

    proof

      let X be RealNormSpace, Y be Subset of X, v be object;

      assume

       A1: v in the carrier of X;

      reconsider Z = Y as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      hereby

        assume v in ( Cl Y);

        then

         A2: v in ( Cl Z) by EQCL1;

        thus for G be Subset of X st G is open & v in G holds G meets Y

        proof

          let G be Subset of X;

          assume

           A3: G is open & v in G;

          reconsider G0 = G as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

          G0 is open by A3, NORMSP_2: 33;

          hence G meets Y by A2, A3, PRE_TOPC:def 7;

        end;

      end;

      assume

       A4: for G be Subset of X st G is open & v in G holds G meets Y;

      

       A5: for G0 be Subset of ( LinearTopSpaceNorm X) st G0 is open & v in G0 holds G0 meets Z

      proof

        let G0 be Subset of ( LinearTopSpaceNorm X);

        assume

         A6: G0 is open & v in G0;

        reconsider G = G0 as Subset of X by NORMSP_2:def 4;

        G is open by A6, NORMSP_2: 33;

        hence G0 meets Z by A4, A6;

      end;

      v in the carrier of ( LinearTopSpaceNorm X) by A1, NORMSP_2:def 4;

      then v in ( Cl Z) by A5, PRE_TOPC:def 7;

      hence v in ( Cl Y) by EQCL1;

    end;

    theorem :: NORMSP_3:6

    

     EQCL3: for X be RealNormSpace, Y be Subset of X, v be object holds v in ( Cl Y) iff ex seq be sequence of X st ( rng seq) c= Y & seq is convergent & ( lim seq) = v

    proof

      let X be RealNormSpace, Y be Subset of X, v be object;

      reconsider Z = Y as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      

       A1: ( Cl Z) = ( Cl Y) by EQCL1;

      hereby

        assume

         A2: v in ( Cl Y);

        then

         A3: for G be Subset of ( LinearTopSpaceNorm X) st G is open & v in G holds G meets Z by A1, PRE_TOPC:def 7;

        reconsider v0 = v as Point of X by A2;

        defpred P[ Nat, Point of X] means ||.(v0 - $2).|| < (1 / ($1 + 1)) & $2 in Y;

        

         A4: for n be Element of NAT holds ex w be Element of X st P[n, w]

        proof

          let n be Element of NAT ;

          set e = (1 / (n + 1));

          for x be object st x in { y where y be Point of X : ||.(v0 - y).|| < e } holds x in the carrier of ( LinearTopSpaceNorm X)

          proof

            let x be object;

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

            then ex y be Point of X st x = y & ||.(v0 - y).|| < e;

            then x in the carrier of X;

            hence thesis by NORMSP_2:def 4;

          end;

          then

          reconsider G = { y where y be Point of X : ||.(v0 - y).|| < e } as Subset of ( LinearTopSpaceNorm X) by TARSKI:def 3;

           ||.(v0 - v0).|| < e by NORMSP_1: 6;

          then v0 in G;

          then G meets Z by A3, NORMSP_2: 23;

          then

          consider w be object such that

           A5: w in (G /\ Z) by XBOOLE_0:def 1;

          

           A6: w in G & w in Z by A5, XBOOLE_0:def 4;

          then

           A7: ex y be Point of X st w = y & ||.(v0 - y).|| < e;

          reconsider w as Point of X by A6;

          take w;

          thus thesis by A5, A7, XBOOLE_0:def 4;

        end;

        consider seq be Function of NAT , X such that

         A8: for n be Element of NAT holds P[n, (seq . n)] from FUNCT_2:sch 3( A4);

        take seq;

        for y be object st y in ( rng seq) holds y in Y

        proof

          let y be object;

          assume y in ( rng seq);

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

          hence thesis by A8;

        end;

        hence ( rng seq) c= Y;

         A10:

        now

          let s be Real;

          consider n be Nat such that

           A11: (s " ) < n by SEQ_4: 3;

          assume

           A12: 0 < s;

          ((s " ) + 0 ) < (n + 1) by A11, XREAL_1: 8;

          then (1 / (n + 1)) < (1 / (s " )) by A12, XREAL_1: 76;

          then

           A13: (1 / (n + 1)) < s by XCMPLX_1: 216;

          take k = n;

          let m be Nat;

          

           A14: m in NAT by ORDINAL1:def 12;

          assume k <= m;

          then (k + 1) <= (m + 1) by XREAL_1: 6;

          then (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

          then (1 / (m + 1)) < s by A13, XXREAL_0: 2;

          then ||.(v0 - (seq . m)).|| < s by A8, A14, XXREAL_0: 2;

          hence ||.((seq . m) - v0).|| < s by NORMSP_1: 7;

        end;

        hence seq is convergent;

        hence ( lim seq) = v by A10, NORMSP_1:def 7;

      end;

      given seq be sequence of X such that

       A15: ( rng seq) c= Y and

       A16: seq is convergent and

       A17: ( lim seq) = v;

      v in the carrier of X by A17;

      then

       A18: v in the carrier of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      reconsider v0 = v as Point of X by A17;

      for G be Subset of ( LinearTopSpaceNorm X) st G is open & v in G holds G meets Z

      proof

        let G be Subset of ( LinearTopSpaceNorm X);

        assume G is open & v in G;

        then

        consider r be Real such that

         A20: r > 0 & { y where y be Point of X : ||.(v0 - y).|| < r } c= G by NORMSP_2: 22;

        consider m be Nat such that

         A21: for n be Nat st m <= n holds ||.((seq . n) - v0).|| < r by A16, A17, A20, NORMSP_1:def 7;

         ||.((seq . m) - v0).|| < r by A21;

        then ||.(v0 - (seq . m)).|| < r by NORMSP_1: 7;

        then

         A22: (seq . m) in { y where y be Point of X : ||.(v0 - y).|| < r };

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

        hence G meets Z by A15, A20, A22, XBOOLE_0:def 4;

      end;

      hence v in ( Cl Y) by A1, A18, PRE_TOPC:def 7;

    end;

    theorem :: NORMSP_3:7

    for X be RealNormSpace, A be Subset of X holds ex F be Subset-Family of X st (for C be Subset of X holds C in F iff C is closed & A c= C) & ( Cl A) = ( meet F)

    proof

      let X be RealNormSpace, A be Subset of X;

      reconsider B = A as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      consider G be Subset-Family of ( LinearTopSpaceNorm X) such that

       A1: (for C be Subset of ( LinearTopSpaceNorm X) holds C in G iff C is closed & B c= C) & ( Cl B) = ( meet G) by PRE_TOPC: 16;

      reconsider F = G as Subset-Family of X by NORMSP_2:def 4;

      for C be Subset of X holds C in F iff C is closed & A c= C

      proof

        let C be Subset of X;

        reconsider D = C as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

        D in G iff D is closed & B c= D by A1;

        hence thesis by NORMSP_2: 32;

      end;

      hence thesis by A1, EQCL1;

    end;

    theorem :: NORMSP_3:8

    for X be RealNormSpace, A,B be Subset of X st A c= B holds ( Cl A) c= ( Cl B)

    proof

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

      assume

       A1: A c= B;

      reconsider A1 = A, B1 = B as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      

       A2: ( Cl A1) = ( Cl A) by EQCL1;

      ( Cl B1) = ( Cl B) by EQCL1;

      hence thesis by A1, A2, PRE_TOPC: 19;

    end;

    theorem :: NORMSP_3:9

    for X be RealNormSpace, A,B be Subset of X holds ( Cl (A \/ B)) = (( Cl A) \/ ( Cl B))

    proof

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

      reconsider A1 = A, B1 = B as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      

       A1: ( Cl A1) = ( Cl A) by EQCL1;

      

       A2: ( Cl B1) = ( Cl B) by EQCL1;

      ( Cl (A1 \/ B1)) = ( Cl (A \/ B)) by EQCL1;

      hence thesis by A1, A2, PRE_TOPC: 20;

    end;

    theorem :: NORMSP_3:10

    for X be RealNormSpace, A,B be Subset of X holds ( Cl (A /\ B)) c= (( Cl A) /\ ( Cl B))

    proof

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

      reconsider A1 = A, B1 = B as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      

       A1: ( Cl A1) = ( Cl A) by EQCL1;

      

       A2: ( Cl B1) = ( Cl B) by EQCL1;

      ( Cl (A1 /\ B1)) = ( Cl (A /\ B)) by EQCL1;

      hence thesis by A1, A2, PRE_TOPC: 21;

    end;

    theorem :: NORMSP_3:11

    for X be RealNormSpace, A be Subset of X holds A is closed iff ( Cl A) = A

    proof

      let X be RealNormSpace, A be Subset of X;

      reconsider A1 = A as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      

       A1: ( Cl A1) = ( Cl A) by EQCL1;

      A1 is closed iff A is closed by NORMSP_2: 32;

      hence thesis by A1, PRE_TOPC: 22;

    end;

    theorem :: NORMSP_3:12

    for X be RealNormSpace, A be Subset of X holds A is open iff ( Cl (( [#] X) \ A)) = (( [#] X) \ A)

    proof

      let X be RealNormSpace, A be Subset of X;

      reconsider A1 = A as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      

       A1: ( [#] X) = ( [#] ( LinearTopSpaceNorm X)) by NORMSP_2:def 4;

      

       A2: ( Cl (( [#] ( LinearTopSpaceNorm X)) \ A1)) = ( Cl (( [#] X) \ A)) by A1, EQCL1;

      A1 is open iff A is open by NORMSP_2: 33;

      hence thesis by A1, A2, PRE_TOPC: 23;

    end;

    theorem :: NORMSP_3:13

    

     Cl01: for X be RealNormSpace, Y be Subspace of X, CY be Subset of X st CY = the carrier of Y holds ( Cl CY) is linearly-closed

    proof

      let X be RealNormSpace, Y be Subspace of X, CY be Subset of X;

      assume

       A1: CY = the carrier of Y;

      

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

      proof

        let v,u be Point of X;

        assume

         A3: v in ( Cl CY) & u in ( Cl CY);

        thus (v + u) in ( Cl CY)

        proof

          consider seqv be sequence of X such that

           A4: ( rng seqv) c= CY & seqv is convergent & ( lim seqv) = v by A3, EQCL3;

          consider sequ be sequence of X such that

           A5: ( rng sequ) c= CY & sequ is convergent & ( lim sequ) = u by A3, EQCL3;

          now

            let y be object;

            assume y in ( rng (seqv + sequ));

            then

            consider x be object such that

             A6: x in NAT & ((seqv + sequ) . x) = y by FUNCT_2: 11;

            reconsider x as Element of NAT by A6;

            (seqv . x) in ( rng seqv) & (sequ . x) in ( rng sequ) by FUNCT_2: 4;

            then (seqv . x) in Y & (sequ . x) in Y by A1, A4, A5;

            then ((seqv . x) + (sequ . x)) in Y by RLSUB_1: 20;

            hence y in CY by A1, A6, NORMSP_1:def 2;

          end;

          then

           A7: ( rng (seqv + sequ)) c= CY;

          ( lim (seqv + sequ)) = (v + u) by A4, A5, NORMSP_1: 25;

          hence (v + u) in ( Cl CY) by A4, A5, A7, EQCL3, NORMSP_1: 19;

        end;

      end;

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

      proof

        let r be Real, v be Point of X;

        assume

         A8: v in ( Cl CY);

        thus (r * v) in ( Cl CY)

        proof

          consider seqv be sequence of X such that

           A9: ( rng seqv) c= CY & seqv is convergent & ( lim seqv) = v by A8, EQCL3;

          

           A10: (r * seqv) is convergent & ( lim (r * seqv)) = (r * ( lim seqv)) by A9, NORMSP_1: 22, NORMSP_1: 28;

          now

            let y be object;

            assume y in ( rng (r * seqv));

            then

            consider x be object such that

             A11: x in NAT & ((r * seqv) . x) = y by FUNCT_2: 11;

            reconsider x as Element of NAT by A11;

            (seqv . x) in ( rng seqv) by FUNCT_2: 4;

            then (seqv . x) in Y by A1, A9;

            then (r * (seqv . x)) in Y by RLSUB_1: 21;

            hence y in CY by A1, A11, NORMSP_1:def 5;

          end;

          then ( rng (r * seqv)) c= CY;

          hence (r * v) in ( Cl CY) by A9, A10, EQCL3;

        end;

      end;

      hence thesis by A2;

    end;

    begin

    definition

      let X be RealNormSpace, A be Subset of X;

      :: NORMSP_3:def2

      attr A is dense means ( Cl A) = ( [#] X);

    end

    registration

      let X be RealNormSpace;

      cluster ( [#] X) -> dense;

      correctness

      proof

        

         A1: ( Cl ( [#] ( LinearTopSpaceNorm X))) = ( [#] ( LinearTopSpaceNorm X)) by TOPS_1:def 3;

        ( [#] ( LinearTopSpaceNorm X)) = ( [#] X) by NORMSP_2:def 4;

        hence thesis by A1, EQCL1;

      end;

    end

    registration

      let X be RealNormSpace;

      cluster open closed dense for Subset of X;

      correctness

      proof

        take ( [#] X);

        thus thesis;

      end;

    end

    theorem :: NORMSP_3:14

    for X be RealNormSpace, A be Subset of X holds A is dense iff for x be Point of X holds ex seq be sequence of X st ( rng seq) c= A & seq is convergent & ( lim seq) = x

    proof

      let X be RealNormSpace, A be Subset of X;

      thus A is dense implies for x be Point of X holds ex seq be sequence of X st ( rng seq) c= A & seq is convergent & ( lim seq) = x by EQCL3;

      assume

       A1: for x be Point of X holds ex seq be sequence of X st ( rng seq) c= A & seq is convergent & ( lim seq) = x;

      for z be object st z in ( [#] X) holds z in ( Cl A)

      proof

        let z be object;

        assume z in ( [#] X);

        then

        reconsider x = z as Point of X;

        ex seq be sequence of X st ( rng seq) c= A & seq is convergent & ( lim seq) = x by A1;

        hence thesis by EQCL3;

      end;

      then ( [#] X) c= ( Cl A);

      then ( [#] X) = ( Cl A);

      hence thesis;

    end;

    theorem :: NORMSP_3:15

    

     EQCL2: for X be RealNormSpace, Y be Subset of X, Z be Subset of ( LinearTopSpaceNorm X) st Y = Z holds Y is dense iff Z is dense

    proof

      let X be RealNormSpace, Y be Subset of X, Z be Subset of ( LinearTopSpaceNorm X);

      assume

       A1: Y = Z;

      hereby

        assume Y is dense;

        

        then ( Cl Z) = ( [#] X) by A1, EQCL1

        .= ( [#] ( LinearTopSpaceNorm X)) by NORMSP_2:def 4;

        hence Z is dense;

      end;

      assume Z is dense;

      

      then ( Cl Y) = ( [#] ( LinearTopSpaceNorm X)) by A1, EQCL1

      .= ( [#] X) by NORMSP_2:def 4;

      hence Y is dense;

    end;

    theorem :: NORMSP_3:16

    for X be RealNormSpace, R,S be Subset of X st R is dense & R c= S holds S is dense

    proof

      let X be RealNormSpace, R,S be Subset of X;

      reconsider R1 = R, S1 = S as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      assume R is dense & R c= S;

      then R1 is dense & R1 c= S1 by EQCL2;

      then S1 is dense by TOPS_1: 44;

      hence S is dense by EQCL2;

    end;

    theorem :: NORMSP_3:17

    

     TOPS145: for X be RealNormSpace, R be Subset of X holds R is dense iff for S be Subset of X st S <> {} & S is open holds R meets S

    proof

      let X be RealNormSpace, R be Subset of X;

      reconsider R1 = R as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      hereby

        assume R is dense;

        then

         A1: R1 is dense by EQCL2;

        thus for S be Subset of X st S <> {} & S is open holds R meets S

        proof

          let S be Subset of X;

          assume

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

          reconsider S1 = S as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

          S1 is open by A2, NORMSP_2: 33;

          hence R meets S by A1, A2, TOPS_1: 45;

        end;

      end;

      assume

       A3: for S be Subset of X st S <> {} & S is open holds R meets S;

      for S1 be Subset of ( LinearTopSpaceNorm X) st S1 <> {} & S1 is open holds R1 meets S1

      proof

        let S1 be Subset of ( LinearTopSpaceNorm X);

        assume

         A4: S1 <> {} & S1 is open;

        reconsider S = S1 as Subset of X by NORMSP_2:def 4;

        S is open by A4, NORMSP_2: 33;

        hence R1 meets S1 by A3, A4;

      end;

      then R1 is dense by TOPS_1: 45;

      hence R is dense by EQCL2;

    end;

    theorem :: NORMSP_3:18

    for X be RealNormSpace, R,S be Subset of X st R is dense & S is open holds ( Cl S) = ( Cl (S /\ R))

    proof

      let X be RealNormSpace, R,S be Subset of X;

      reconsider R1 = R, S1 = S as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      

       A1: ( Cl S) = ( Cl S1) by EQCL1;

      

       A2: ( Cl (S1 /\ R1)) = ( Cl (S /\ R)) by EQCL1;

      assume R is dense & S is open;

      then R1 is dense & S1 is open by EQCL2, NORMSP_2: 33;

      hence ( Cl S) = ( Cl (S /\ R)) by A1, A2, TOPS_1: 46;

    end;

    theorem :: NORMSP_3:19

    for X be RealNormSpace, R,S be Subset of X st R is dense & S is dense open holds (R /\ S) is dense

    proof

      let X be RealNormSpace, R,S be Subset of X;

      reconsider R1 = R, S1 = S as Subset of ( LinearTopSpaceNorm X) by NORMSP_2:def 4;

      assume R is dense & S is dense open;

      then R1 is dense & S1 is dense & S1 is open by EQCL2, NORMSP_2: 33;

      then (R1 /\ S1) is dense by TOPS_1: 47;

      hence (R /\ S) is dense by EQCL2;

    end;

    theorem :: NORMSP_3:20

    

     NONEMP: for X be RealNormSpace, A be Subset of X st A is dense holds A is non empty

    proof

      let X be RealNormSpace, A be Subset of X;

      assume A is dense;

      then A meets ( [#] X) by TOPS145;

      hence A is non empty;

    end;

    begin

    definition

      let X be RealNormSpace;

      :: NORMSP_3:def3

      attr X is separable means ( LinearTopSpaceNorm X) is separable;

    end

    theorem :: NORMSP_3:21

    for X be RealNormSpace holds X is separable iff ex seq be sequence of X st ( rng seq) is dense

    proof

      let X be RealNormSpace;

      set Y = ( LinearTopSpaceNorm X);

      consider B be Subset of Y such that

       A1: B is dense & ( density Y) = ( card B) by TOPGEN_1:def 12;

      hereby

        assume

         A2: X is separable;

        reconsider A = B as Subset of X by NORMSP_2:def 4;

        A is dense by A1, EQCL2;

        then

         A3: A is non empty by NONEMP;

        A is countable by A1, A2, CARD_3:def 14, TOPGEN_1:def 13;

        then

        consider f be Function of omega , A such that

         A4: ( rng f) = A by A3, CARD_3: 96;

        reconsider seq = f as Function of NAT , the carrier of X by A3, A4, FUNCT_2: 6;

        reconsider seq as sequence of X;

        ( rng seq) is dense by A1, A4, EQCL2;

        hence ex seq be sequence of X st ( rng seq) is dense;

      end;

      given seq be sequence of X such that

       A5: ( rng seq) is dense;

      reconsider D = ( rng seq) as Subset of Y by NORMSP_2:def 4;

      D is dense by A5, EQCL2;

      then

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

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

      then ( card D) c= omega by CARD_3: 93, CARD_3:def 14;

      then ( density Y) c= omega by A6;

      hence thesis by TOPGEN_1:def 13;

    end;

    begin

    theorem :: NORMSP_3:22

    

     LMINEQ: for x,y,z be Real st 0 <= y & for e be Real st 0 < e holds x <= (z + (y * e)) holds x <= z

    proof

      let x,y,z be Real such that

       A1: 0 <= y and

       A2: for e be Real st 0 < e holds x <= (z + (y * e));

      per cases ;

        suppose

         A3: y = 0 ;

        x <= (z + (y * 1)) by A2;

        hence x <= z by A3;

      end;

        suppose

         A4: y <> 0 ;

        thus x <= z

        proof

          assume not x <= z;

          then

           A6: 0 < (x - z) by XREAL_1: 50;

          then x <= (z + (y * (((x - z) / 2) / y))) by A1, A2, A4;

          then

           A7: x <= (z + ((y * ((x - z) / 2)) / y)) by XCMPLX_1: 74;

          ((x - z) / 2) < (x - z) by A6, XREAL_1: 216;

          then (z + ((x - z) / 2)) < (z + (x - z)) by XREAL_1: 8;

          hence contradiction by A4, A7, XCMPLX_1: 89;

        end;

      end;

    end;

    theorem :: NORMSP_3:23

    

     CLOSE01: for X be RealNormSpace, x be Point of X, seq be sequence of X st for n be Nat holds (seq . n) = x holds seq is convergent & ( lim seq) = x

    proof

      let X be RealNormSpace, x be Point of X, seq be sequence of X;

      assume

       A1: for n be Nat holds (seq . n) = x;

      now

        let z,w be object;

        assume z in ( dom seq) & w in ( dom seq);

        then

        reconsider n1 = z, n2 = w as Nat;

        

        thus (seq . z) = (seq . n1)

        .= x by A1

        .= (seq . n2) by A1

        .= (seq . w);

      end;

      then

       A2: seq is constant by FUNCT_1:def 10;

      hence seq is convergent by NDIFF_1: 18;

      

      thus ( lim seq) = (seq . 0 ) by A2, NDIFF_1: 18

      .= x by A1;

    end;

    theorem :: NORMSP_3:24

    for X be RealNormSpace, x be Point of X holds {x} is closed

    proof

      let X be RealNormSpace, x be Point of X;

      for s1 be sequence of X st ( rng s1) c= {x} & s1 is convergent holds ( lim s1) in {x}

      proof

        let s1 be sequence of X;

        assume

         A1: ( rng s1) c= {x} & s1 is convergent;

        now

          let n be Nat;

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

          hence (s1 . n) = x by A1, TARSKI:def 1;

        end;

        then ( lim s1) = x by CLOSE01;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: NORMSP_3:25

    

     CLOSE1: for X be RealNormSpace, Y be Subset of X, v be VECTOR of X st Y is closed & for e be Real st 0 < e holds ex w be VECTOR of X st w in Y & ||.(v - w).|| <= e holds v in Y

    proof

      let X be RealNormSpace, Y be Subset of X, v be VECTOR of X;

      assume that

       A1: Y is closed and

       A2: for e be Real st 0 < e holds ex w be VECTOR of X st w in Y & ||.(v - w).|| <= e;

      assume

       A3: not v in Y;

      reconsider Z = (Y ` ) as Subset of ( TopSpaceNorm X);

      

       A4: Z is open by A1, NORMSP_2: 16;

      v in (the carrier of X \ Y) by A3, XBOOLE_0:def 5;

      then v in Z by SUBSET_1:def 4;

      then

      consider e be Real such that

       A5: e > 0 & { y where y be Point of X : ||.(v - y).|| < e } c= Z by A4, NORMSP_2: 7;

      consider w be VECTOR of X such that

       A6: w in Y & ||.(v - w).|| <= (e / 2) by A2, A5;

      (e / 2) < e by A5, XREAL_1: 216;

      then ||.(v - w).|| < e by A6, XXREAL_0: 2;

      then w in { y where y be Point of X : ||.(v - y).|| < e };

      then w in (Y ` ) by A5;

      then w in (the carrier of X \ Y) by SUBSET_1:def 4;

      hence contradiction by A6, XBOOLE_0:def 5;

    end;

    begin

    theorem :: NORMSP_3:26

    

     NSUBA: for V be RealNormSpace, W be SubRealNormSpace of V st the carrier of W = the carrier of V holds the NORMSTR of W = the NORMSTR of V

    proof

      let V be RealNormSpace, W be SubRealNormSpace of V;

      assume

       A1: the carrier of W = the carrier of V;

      

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

      

       A3: the addF of W = (the addF of V || the carrier of W) by DUALSP01:def 16

      .= the addF of V by A1;

      

       A4: the Mult of W = (the Mult of V | [: REAL , the carrier of W:]) by DUALSP01:def 16

      .= the Mult of V by A1;

      the normF of W = (the normF of V | the carrier of W) by DUALSP01:def 16

      .= the normF of V by A1;

      hence thesis by A2, A3, A4;

    end;

    theorem :: NORMSP_3:27

    for V be RealNormSpace, W be SubRealNormSpace of V holds W is Subspace of V

    proof

      let V be RealNormSpace, W be SubRealNormSpace of V;

      the carrier of W c= the carrier of V & ( 0. W) = ( 0. V) & the addF of W = (the addF of V || the carrier of W) & the Mult of W = (the Mult of V | [: REAL , the carrier of W:]) & the normF of W = (the normF of V | the carrier of W) by DUALSP01:def 16;

      hence thesis by RLSUB_1:def 2;

    end;

    theorem :: NORMSP_3:28

    

     SUBTH0: for V be RealNormSpace, V1 be SubRealNormSpace of V, x,y be Point of V, x1,y1 be Point of V1, a be Real st x = x1 & y = y1 holds ||.x.|| = ||.x1.|| & (x + y) = (x1 + y1) & (a * x) = (a * x1)

    proof

      let V be RealNormSpace, V1 be SubRealNormSpace of V, x,y be Point of V, x1,y1 be Point of V1, a be Real;

      assume

       A1: x = x1 & y = y1;

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

      

      thus ||.x1.|| = ((the normF of V | the carrier of V1) . x1) by DUALSP01:def 16

      .= ||.x.|| by A1, FUNCT_1: 49;

      

      thus (x1 + y1) = ((the addF of V || the carrier of V1) . [x1, y1]) by DUALSP01:def 16

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

      

       A2: [aa, x1] in [: REAL , the carrier of V1:];

      (aa * x1) = ((the Mult of V | [: REAL , the carrier of V1:]) . [a, x1]) by DUALSP01:def 16

      .= (aa * x) by A1, A2, FUNCT_1: 49;

      hence (a * x) = (a * x1);

    end;

    theorem :: NORMSP_3:29

    

     RLSUB134: for V be RealNormSpace, V1 be SubRealNormSpace of V, S be Subset of V st S = the carrier of V1 holds S is linearly-closed

    proof

      let V be RealNormSpace, V1 be SubRealNormSpace of V, S be Subset of V;

      assume

       A1: S = the carrier of V1;

      

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

      proof

        let v,u be VECTOR of V such that

         A3: v in S and

         A4: u in S;

        reconsider v1 = v, u1 = u as Point of V1 by A1, A3, A4;

        (v + u) = (v1 + u1) by SUBTH0;

        hence thesis by A1;

      end;

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

      proof

        let r be Real;

        let v be VECTOR of V such that

         A5: v in S;

        reconsider v1 = v as Point of V1 by A1, A5;

        (r * v) = (r * v1) by SUBTH0;

        hence thesis by A1;

      end;

      hence thesis by A2;

    end;

    definition

      let X be RealNormSpace;

      let X1 be set;

      assume

       A1: X1 c= the carrier of X;

      :: NORMSP_3:def4

      func Norm_ (X1,X) -> Function of X1, REAL equals

      : DefNorm: (the normF of X | X1);

      correctness

      proof

        

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

        

         A3: for z be object st z in X1 holds ((the normF of X | X1) . z) in REAL

        proof

          let z be object;

          assume

           A4: z in X1;

          then

          reconsider y = z as VECTOR of X by A1;

          z in ( dom (the normF of X | X1)) by A1, A2, A4, RELAT_1: 62;

          then ((the normF of X | X1) . z) = ||.y.|| by FUNCT_1: 47;

          hence ((the normF of X | X1) . z) in REAL ;

        end;

        ( dom (the normF of X | X1)) = X1 by A1, A2, RELAT_1: 62;

        hence (the normF of X | X1) is Function of X1, REAL by A3, FUNCT_2: 3;

      end;

    end

    definition

      let V be RealNormSpace, V1 be Subset of V;

      :: NORMSP_3:def5

      func NLin (V1) -> non empty NORMSTR equals NORMSTR (# the carrier of ( Lin V1), ( 0. ( Lin V1)), the addF of ( Lin V1), the Mult of ( Lin V1), ( Norm_ (the carrier of ( Lin V1),V)) #);

      correctness ;

    end

    

     SUBTH: for V be RealNormSpace, V1 be Subset of V, x,y be Point of V, x1,y1 be Point of ( NLin V1), a be Real st x = x1 & y = y1 holds ||.x.|| = ||.x1.|| & (x + y) = (x1 + y1) & (a * x) = (a * x1)

    proof

      let V be RealNormSpace, V1 be Subset of V, x,y be Point of V, x1,y1 be Point of ( NLin V1), a be Real;

      assume

       A1: x = x1 & y = y1;

      set l = ( NLin V1);

      

       A2: the carrier of l c= the carrier of V by RLSUB_1:def 2;

      reconsider x2 = x1 as Point of ( Lin V1);

      reconsider y2 = y1 as Point of ( Lin V1);

      

      thus ||.x1.|| = ((the normF of V | the carrier of l) . x1) by A2, DefNorm

      .= ||.x.|| by A1, FUNCT_1: 49;

      

      thus (x1 + y1) = (x2 + y2)

      .= (x + y) by A1, RLSUB_1: 13;

      

      thus (a * x1) = (a * x2)

      .= (a * x) by A1, RLSUB_1: 14;

    end;

    

     XTh7: for V be RealNormSpace, V1 be Subset of V, x,y be Point of ( NLin V1), a be Real holds ( ||.x.|| = 0 iff x = ( 0. ( NLin V1))) & 0 <= ||.x.|| & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) & ||.(a * x).|| = ( |.a.| * ||.x.||)

    proof

      let V be RealNormSpace, V1 be Subset of V;

      let x,y be Point of ( NLin V1), a be Real;

      set l = ( NLin V1);

      the carrier of l c= the carrier of V by RLSUB_1:def 2;

      then

      reconsider x0 = x, y0 = y as Point of V;

      

       A1: ||.x.|| = ||.x0.|| by SUBTH;

      

       A2: ||.y.|| = ||.y0.|| by SUBTH;

      

       A3: ( 0. ( NLin V1)) = ( 0. V) by RLSUB_1: 11;

      (x + y) = (x0 + y0) by SUBTH;

      then

       A4: ||.(x0 + y0).|| = ||.(x + y).|| by SUBTH;

      (a * x) = (a * x0) by SUBTH;

      then

       A5: ||.(a * x0).|| = ||.(a * x).|| by SUBTH;

      thus ( ||.x.|| = 0 iff x = ( 0. ( NLin V1))) by A1, A3, NORMSP_0:def 5;

      thus 0 <= ||.x.|| by A1;

      thus ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by A1, A2, A4, NORMSP_1:def 1;

      thus ||.(a * x).|| = ( |.a.| * ||.x.||) by A1, A5, NORMSP_1:def 1;

    end;

    theorem :: NORMSP_3:30

    

     ThSubSpace: for V be RealNormSpace, V1 be Subset of V holds ( NLin V1) is SubRealNormSpace of V

    proof

      let V be RealNormSpace;

      let V1 be Subset of V;

      set l = ( NLin V1);

      

       A1: the carrier of l c= the carrier of V by RLSUB_1:def 2;

      

       A2: l is reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable by RSSPACE: 15, XTh7;

      

       A3: ( 0. l) = ( 0. V) by RLSUB_1:def 2;

      

       A4: the addF of l = (the addF of V || the carrier of l) by RLSUB_1:def 2;

      

       A5: the Mult of l = (the Mult of V | [: REAL , the carrier of l:]) by RLSUB_1:def 2;

      the normF of l = (the normF of V | the carrier of l) by A1, DefNorm;

      hence thesis by A1, A2, A3, A4, A5, DUALSP01:def 16;

    end;

    definition

      let V be RealNormSpace, V1 be Subset of V;

      :: original: NLin

      redefine

      func NLin (V1) -> SubRealNormSpace of V ;

      coherence by ThSubSpace;

    end

    theorem :: NORMSP_3:31

    

     LCL1: for V be RealLinearSpace, V1 be Subset of V st V1 <> {} & V1 is linearly-closed holds the carrier of ( Lin V1) = V1

    proof

      let V be RealLinearSpace, V1 be Subset of V;

      assume V1 <> {} & V1 is linearly-closed;

      then ex W0 be strict Subspace of V st V1 = the carrier of W0 by RLSUB_1: 35;

      hence the carrier of ( Lin V1) = V1 by RLVECT_3: 18;

    end;

    theorem :: NORMSP_3:32

    for V be RealNormSpace, W be SubRealNormSpace of V, V1 be Subset of V st the carrier of W = V1 holds ( NLin V1) = the NORMSTR of W

    proof

      let V be RealNormSpace, W be SubRealNormSpace of V, V1 be Subset of V;

      assume

       A1: the carrier of W = V1;

      set l = ( NLin V1);

      

       A2: the carrier of l c= the carrier of V by RLSUB_1:def 2;

      

       A3: the carrier of l = the carrier of W by A1, LCL1, RLSUB134;

      

       A4: ( 0. l) = ( 0. V) by RLSUB_1:def 2;

      

       A5: the addF of l = (the addF of V || the carrier of l) by RLSUB_1:def 2;

      

       A6: the Mult of l = (the Mult of V | [: REAL , the carrier of l:]) by RLSUB_1:def 2;

      

       A7: ( 0. W) = ( 0. l) by A4, DUALSP01:def 16;

      

       A8: the addF of W = the addF of l by A3, A5, DUALSP01:def 16;

      the normF of W = (the normF of V | the carrier of W) by DUALSP01:def 16

      .= the normF of l by A2, A3, DefNorm;

      hence thesis by A6, A7, A8, DUALSP01:def 16;

    end;

    begin

    theorem :: NORMSP_3:33

    

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

    proof

      let X,Y be RealLinearSpace, f be Function of X, Y;

      assume

       A1: f is homogeneous;

      (f . ( 0. X)) = (f . ( 0 * ( 0. X))) by RLVECT_1: 10

      .= ( 0 * (f . ( 0. X))) by A1, LOPBAN_1:def 5

      .= ( 0. Y) by RLVECT_1: 10;

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

      hence thesis by FUNCT_2: 38;

    end;

    registration

      let X,Y be RealLinearSpace, f be LinearOperator of X, Y;

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

      correctness by KERX1;

    end

    theorem :: NORMSP_3:34

    

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

    proof

      let X,Y be RealLinearSpace, f be Function of X, Y;

      assume

       A1: f is additive homogeneous;

      set X1 = (f " {( 0. Y)});

      

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

      proof

        let v,u be Point of X;

        assume

         AS1: v in X1 & u in X1;

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

        then

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

        

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

        (f . (v + u)) = ((f . v) + (f . u)) by A1

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

        .= ( 0. Y) by RLVECT_1: 4;

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

        hence thesis by FUNCT_2: 38;

      end;

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

      proof

        let r be Real, v be Point of X;

        assume v in X1;

        then

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

        (f . (r * v)) = (r * (f . v)) by A1, LOPBAN_1:def 5

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

        .= ( 0. Y) by RLVECT_1: 10;

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

        hence thesis by FUNCT_2: 38;

      end;

      hence thesis by A2;

    end;

    theorem :: NORMSP_3:35

    

     IMX2: for X,Y be RealLinearSpace, f be Function of X, Y st f is additive homogeneous holds ( rng f) is linearly-closed

    proof

      let X,Y be RealLinearSpace, f be Function of X, Y;

      assume

       A1: f is additive homogeneous;

      set Y1 = ( rng f);

      

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

      proof

        let v,u be Point of Y;

        assume

         A3: v in Y1 & u in Y1;

        then

        consider x1 be Element of the carrier of X such that

         A4: v = (f . x1) by FUNCT_2: 113;

        consider x2 be Element of the carrier of X such that

         A5: u = (f . x2) by A3, FUNCT_2: 113;

        (v + u) = (f . (x1 + x2)) by A1, A4, A5;

        hence thesis by FUNCT_2: 4;

      end;

      for r be Real, v be Point of Y st v in Y1 holds (r * v) in Y1

      proof

        let r be Real, v be Point of Y;

        assume v in Y1;

        then

        consider x be Element of the carrier of X such that

         A6: v = (f . x) by FUNCT_2: 113;

        (r * v) = (f . (r * x)) by A1, A6, LOPBAN_1:def 5;

        hence thesis by FUNCT_2: 4;

      end;

      hence thesis by A2;

    end;

    definition

      let X,Y be RealLinearSpace, f be LinearOperator of X, Y;

      :: NORMSP_3:def6

      func Ker (f) -> Subspace of X equals ( Lin (f " {( 0. Y)}));

      coherence ;

    end

    definition

      let X,Y be RealNormSpace, f be LinearOperator of X, Y;

      :: NORMSP_3:def7

      func NKer (f) -> SubRealNormSpace of X equals ( NLin (f " {( 0. Y)}));

      coherence ;

    end

    definition

      let X,Y be RealLinearSpace, f be LinearOperator of X, Y;

      :: NORMSP_3:def8

      func Im (f) -> Subspace of Y equals ( Lin ( rng f));

      coherence ;

    end

    definition

      let X,Y be RealNormSpace, f be LinearOperator of X, Y;

      :: NORMSP_3:def9

      func Im (f) -> SubRealNormSpace of Y equals ( NLin ( rng f));

      coherence ;

    end

    definition

      let X,Y be RealLinearSpace, L be LinearOperator of X, Y;

      :: NORMSP_3:def10

      attr L is isomorphism means L is one-to-one onto;

    end

    registration

      let X,Y be RealLinearSpace;

      cluster isomorphism -> one-to-one onto for LinearOperator of X, Y;

      coherence ;

      cluster one-to-one onto -> isomorphism for LinearOperator of X, Y;

      coherence ;

    end

    theorem :: NORMSP_3:36

    for X,Y be RealLinearSpace, L be LinearOperator of X, Y st L is isomorphism holds ex K be LinearOperator of Y, X st K = (L " ) & K is isomorphism

    proof

      let X,Y be RealLinearSpace, L be LinearOperator of X, Y;

      assume

       A1: L is isomorphism;

      then

       A2: L is one-to-one & L is onto;

      reconsider K = (L " ) as Function of Y, X by A2, FUNCT_2: 25;

      

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

      

       A4: K is additive

      proof

        let x,y be Point of Y;

        consider a be Point of X such that

         A5: x = (L . a) by A2, FUNCT_2: 113;

        consider b be Point of X such that

         A6: y = (L . b) by A2, FUNCT_2: 113;

        

         A7: (K . x) = a by A1, A3, A5, FUNCT_1: 34;

        

         A8: (K . y) = b by A1, A3, A6, FUNCT_1: 34;

        (x + y) = (L . (a + b)) by A5, A6, VECTSP_1:def 20;

        hence (K . (x + y)) = ((K . x) + (K . y)) by A1, A3, A7, A8, FUNCT_1: 34;

      end;

      K is homogeneous

      proof

        let x be Point of Y, r be Real;

        consider a be Point of X such that

         A10: x = (L . a) by A2, FUNCT_2: 113;

        

         A11: (K . x) = a by A1, A3, A10, FUNCT_1: 34;

        

         A12: (r * x) = (L . (r * a)) by A10, LOPBAN_1:def 5;

        thus (K . (r * x)) = (r * (K . x)) by A1, A3, A11, A12, FUNCT_1: 34;

      end;

      then

      reconsider K as LinearOperator of Y, X by A4;

      take K;

      K is onto by A1, A3, FUNCT_1: 33;

      hence thesis by A1, FUNCT_1: 40;

    end;

    definition

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

      :: NORMSP_3:def11

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

    end

    registration

      let X,Y be RealNormSpace;

      cluster isomorphism -> one-to-one onto for LinearOperator of X, Y;

      coherence ;

    end

    theorem :: NORMSP_3:37

    

     NISOM01: for X,Y be RealNormSpace, L be LinearOperator of X, Y st L is isomorphism holds ex K be Lipschitzian LinearOperator of Y, X st K = (L " ) & K is isomorphism

    proof

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

      assume

       A1: L is isomorphism;

      then

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

      reconsider K = (L " ) as Function of Y, X by A2, FUNCT_2: 25;

      

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

      

       A4: K is additive

      proof

        let x,y be Point of Y;

        consider a be Point of X such that

         A5: x = (L . a) by A2, FUNCT_2: 113;

        consider b be Point of X such that

         A6: y = (L . b) by A2, FUNCT_2: 113;

        

         A7: (K . x) = a by A1, A3, A5, FUNCT_1: 34;

        

         A8: (K . y) = b by A1, A3, A6, FUNCT_1: 34;

        (x + y) = (L . (a + b)) by A5, A6, VECTSP_1:def 20;

        hence (K . (x + y)) = ((K . x) + (K . y)) by A1, A3, A7, A8, FUNCT_1: 34;

      end;

      K is homogeneous

      proof

        let x be Point of Y, r be Real;

        consider a be Point of X such that

         A10: x = (L . a) by A2, FUNCT_2: 113;

        

         A11: (K . x) = a by A1, A3, A10, FUNCT_1: 34;

        

         A12: (r * x) = (L . (r * a)) by A10, LOPBAN_1:def 5;

        thus (K . (r * x)) = (r * (K . x)) by A1, A3, A11, A12, FUNCT_1: 34;

      end;

      then

      reconsider K as LinearOperator of Y, X by A4;

      

       A13: K is onto by A1, A3, FUNCT_1: 33;

      

       A14: for y be Point of Y holds ||.y.|| = ||.(K . y).||

      proof

        let y be Point of Y;

        consider b be Point of X such that

         A15: y = (L . b) by A2, FUNCT_2: 113;

        (K . y) = b by A1, A3, A15, FUNCT_1: 34;

        hence ||.y.|| = ||.(K . y).|| by A1, A15;

      end;

      then for x be VECTOR of Y holds ||.(K . x).|| <= (1 * ||.x.||);

      then

      reconsider K as Lipschitzian LinearOperator of Y, X by LOPBAN_1:def 8;

      take K;

      thus thesis by A1, A13, A14, FUNCT_1: 40;

    end;

    theorem :: NORMSP_3:38

    

     NISOM02: for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, seq be sequence of X holds seq is convergent implies (L * seq) is convergent & ( lim (L * seq)) = (L . ( lim seq))

    proof

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

      assume

       A1: seq is convergent;

      

       A2: L is_continuous_on the carrier of X by LOPBAN_7: 6;

      

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

      

       A4: ( rng seq) c= the carrier of X;

      ( lim seq) in the carrier of X;

      then

       A5: (L /* seq) is convergent & (L /. ( lim seq)) = ( lim (L /* seq)) by A1, A2, A4, NFCONT_1: 18;

      ( rng seq) c= ( dom L) by A3;

      hence thesis by A5, FUNCT_2:def 11;

    end;

    theorem :: NORMSP_3:39

    

     KERCL01: for X,Y be RealNormSpace, L be Function of X, Y, w be Point of Y st L is_continuous_on the carrier of X holds (L " {w}) is closed

    proof

      let X,Y be RealNormSpace, L be Function of X, Y, w be Point of Y;

      assume

       A1: L is_continuous_on the carrier of X;

      for seq be sequence of X st ( rng seq) c= (L " {w}) & seq is convergent holds ( lim seq) in (L " {w})

      proof

        let seq be sequence of X;

        assume

         A2: ( rng seq) c= (L " {w}) & seq is convergent;

        ( lim seq) in the carrier of X;

        then

         A3: (L /* seq) is convergent & (L /. ( lim seq)) = ( lim (L /* seq)) by A1, A2, NFCONT_1: 18;

        now

          let n be Nat;

          

           A4: n in NAT by ORDINAL1:def 12;

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

          then (L . (seq . n)) in {w} by A2, FUNCT_2: 38;

          then (L . (seq . n)) = w by TARSKI:def 1;

          hence ((L /* seq) . n) = w by A4, FUNCT_2: 115;

        end;

        then ( lim (L /* seq)) = w by CLOSE01;

        then (L /. ( lim seq)) in {w} by A3, TARSKI:def 1;

        hence ( lim seq) in (L " {w}) by FUNCT_2: 38;

      end;

      hence thesis;

    end;

    theorem :: NORMSP_3:40

    for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y holds the carrier of ( Ker L) = (L " {( 0. Y)}) & (L " {( 0. Y)}) is closed by LCL1, KLXY1, KERCL01, LOPBAN_7: 6;

    theorem :: NORMSP_3:41

    

     NISOM03: for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, seq be sequence of X st L is isomorphism holds seq is convergent iff (L * seq) is convergent

    proof

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

      assume

       A1: L is isomorphism;

      

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

      set Lseq = (L * seq);

      set Ls = (L . ( lim seq));

      thus seq is convergent implies Lseq is convergent by NISOM02;

      assume

       A3: Lseq is convergent;

      consider K be Lipschitzian LinearOperator of Y, X such that

       A4: K = (L " ) & K is isomorphism by A1, NISOM01;

      for n be Element of NAT holds ((K * Lseq) . n) = (seq . n)

      proof

        let n be Element of NAT ;

        

         A5: ( dom seq) = NAT by FUNCT_2:def 1;

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

        

        hence ((K * Lseq) . n) = (K . (Lseq . n)) by FUNCT_1: 13

        .= ((L " ) . (L . (seq . n))) by A4, A5, FUNCT_1: 13

        .= (seq . n) by A1, A2, FUNCT_1: 34;

      end;

      then (K * Lseq) = seq;

      hence seq is convergent by A3, NISOM02;

    end;

    theorem :: NORMSP_3:42

    

     NISOM04: for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, seq be sequence of X st L is isomorphism holds seq is Cauchy_sequence_by_Norm implies (L * seq) is Cauchy_sequence_by_Norm

    proof

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

      assume

       A1: L is isomorphism;

      set Lseq = (L * seq);

      assume

       A2: seq is Cauchy_sequence_by_Norm;

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

      proof

        let r be Real;

        assume 0 < r;

        then

        consider k be Nat such that

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

        take k;

        let n,m be Nat;

        assume

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

        

         A5: ( dom seq) = NAT by FUNCT_2:def 1;

        ((Lseq . n) - (Lseq . m)) = ((L . (seq . n)) - ((L * seq) . m)) by A5, FUNCT_1: 13, ORDINAL1:def 12

        .= ((L . (seq . n)) + ( - (L . (seq . m)))) by A5, FUNCT_1: 13, ORDINAL1:def 12

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

        .= ((L . (seq . n)) + (L . (( - 1) * (seq . m)))) by LOPBAN_1:def 5

        .= (L . ((seq . n) + (( - 1) * (seq . m)))) by VECTSP_1:def 20

        .= (L . ((seq . n) - (seq . m))) by RLVECT_1: 16;

        then ||.((Lseq . n) - (Lseq . m)).|| = ||.((seq . n) - (seq . m)).|| by A1;

        hence ||.((Lseq . n) - (Lseq . m)).|| < r by A3, A4;

      end;

      hence thesis by RSSPACE3: 8;

    end;

    theorem :: NORMSP_3:43

    

     NISOM05: for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, seq be sequence of X st L is isomorphism holds seq is Cauchy_sequence_by_Norm iff (L * seq) is Cauchy_sequence_by_Norm

    proof

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

      assume

       A1: L is isomorphism;

      

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

      set Lseq = (L * seq);

      thus seq is Cauchy_sequence_by_Norm implies Lseq is Cauchy_sequence_by_Norm by A1, NISOM04;

      assume

       A3: Lseq is Cauchy_sequence_by_Norm;

      consider K be Lipschitzian LinearOperator of Y, X such that

       A4: K = (L " ) & K is isomorphism by A1, NISOM01;

      for n be Element of NAT holds ((K * Lseq) . n) = (seq . n)

      proof

        let n be Element of NAT ;

        

         A5: ( dom seq) = NAT by FUNCT_2:def 1;

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

        

        hence ((K * Lseq) . n) = (K . (Lseq . n)) by FUNCT_1: 13

        .= ((L " ) . (L . (seq . n))) by A4, A5, FUNCT_1: 13

        .= (seq . n) by A1, A2, FUNCT_1: 34;

      end;

      then (K * Lseq) = seq;

      hence seq is Cauchy_sequence_by_Norm by A3, A4, NISOM04;

    end;

    theorem :: NORMSP_3:44

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

    proof

      let X,Y be RealNormSpace;

      given L be Lipschitzian LinearOperator of X, Y such that

       A1: L is isomorphism;

      hereby

        assume

         A2: X is complete;

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

        proof

          let seq be sequence of Y;

          assume

           A3: seq is Cauchy_sequence_by_Norm;

          consider K be Lipschitzian LinearOperator of Y, X such that

           A4: K = (L " ) & K is isomorphism by A1, NISOM01;

          (K * seq) is Cauchy_sequence_by_Norm by A3, A4, NISOM05;

          then (K * seq) is convergent by A2, LOPBAN_1:def 15;

          hence seq is convergent by A4, NISOM03;

        end;

        hence Y is complete by LOPBAN_1:def 15;

      end;

      assume

       A5: Y is complete;

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

      proof

        let seq be sequence of X;

        assume seq is Cauchy_sequence_by_Norm;

        then (L * seq) is Cauchy_sequence_by_Norm by A1, NISOM05;

        then (L * seq) is convergent by A5, LOPBAN_1:def 15;

        hence seq is convergent by A1, NISOM03;

      end;

      hence X is complete by LOPBAN_1:def 15;

    end;

    

     NISOM06: for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, V be Subset of X, W be Subset of Y st L is isomorphism & W = (L .: V) holds W is closed implies V is closed

    proof

      let X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, V be Subset of X, W be Subset of Y;

      assume

       A1: L is isomorphism & W = (L .: V);

      then

      consider K be Lipschitzian LinearOperator of Y, X such that

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

      

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

      assume

       A4: W is closed;

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

      proof

        let s1 be sequence of X;

        assume

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

        set s2 = (L * s1);

        

         A6: s2 is convergent & ( lim s2) = (L . ( lim s1)) by A5, NISOM02;

        (L .: ( rng s1)) c= (L .: V) by A5, RELAT_1: 123;

        then ( rng s2) c= W by A1, RELAT_1: 127;

        then (L . ( lim s1)) in (L .: V) by A1, A4, A6;

        then ((L " ) . (L . ( lim s1))) in (K .: (L .: V)) by A2, FUNCT_2: 35;

        then

         A8: ( lim s1) in (K .: (L .: V)) by A1, A3, FUNCT_1: 34;

        

         A9: (K .: (L .: V)) = (L " (L .: V)) by A1, A2, FUNCT_1: 85;

        (L " (L .: V)) c= V by A1, FUNCT_1: 82;

        hence ( lim s1) in V by A8, A9;

      end;

      hence V is closed;

    end;

    theorem :: NORMSP_3:45

    for X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, V be Subset of X, W be Subset of Y st L is isomorphism & W = (L .: V) holds V is closed iff W is closed

    proof

      let X,Y be RealNormSpace, L be Lipschitzian LinearOperator of X, Y, V be Subset of X, W be Subset of Y;

      assume

       A1: L is isomorphism & W = (L .: V);

      then

      consider K be Lipschitzian LinearOperator of Y, X such that

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

      

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

      (K .: (L .: V)) = (L " (L .: V)) by A1, A2, FUNCT_1: 85;

      then V = (K .: W) by A1, A3, FUNCT_1: 76, FUNCT_1: 82;

      hence V is closed implies W is closed by A2, NISOM06;

      thus thesis by A1, NISOM06;

    end;

    theorem :: NORMSP_3:46

    for X,Y be RealNormSpace, L be LinearOperator of X, Y st L is onto holds ( Im L) = the NORMSTR of Y

    proof

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

      assume L is onto;

      then the carrier of ( Im L) = the carrier of Y by LCL1, IMX2;

      hence ( Im L) = the NORMSTR of Y by NSUBA;

    end;

    begin

    theorem :: NORMSP_3:47

    

     LM76A: for V be RealBanachSpace, V1 be SubRealNormSpace of V st ex CV1 be Subset of V st CV1 = the carrier of V1 & CV1 is closed holds V1 is RealBanachSpace

    proof

      let V be RealBanachSpace, V1 be SubRealNormSpace of V;

      given CV1 be Subset of V such that

       A1: CV1 = the carrier of V1 & CV1 is closed;

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

      proof

        let seq be sequence of V1;

        assume

         A2: seq is Cauchy_sequence_by_Norm;

        the carrier of V1 c= the carrier of V by DUALSP01:def 16;

        then

        reconsider seq1 = seq as sequence of V by FUNCT_2: 7;

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

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider k be Nat such that

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

          take k;

          let n,m be Nat;

          assume n >= k & m >= k;

          then

           A4: ||.((seq . n) - (seq . m)).|| < r by A3;

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

          .= (( - 1) * (seq1 . m)) by SUBTH0

          .= ( - (seq1 . m)) by RLVECT_1: 16;

          then ((seq . n) - (seq . m)) = ((seq1 . n) - (seq1 . m)) by SUBTH0;

          hence ||.((seq1 . n) - (seq1 . m)).|| < r by A4, SUBTH0;

        end;

        then

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

        ( rng seq) c= CV1 by A1;

        then

        reconsider s = ( lim seq1) as Point of V1 by A1, A6;

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

        proof

          let r be Real;

          assume r > 0 ;

          then

          consider m be Nat such that

           A7: for n be Nat st m <= n holds ||.((seq1 . n) - ( lim seq1)).|| < r by A6, NORMSP_1:def 7;

          take m;

          let n be Nat;

          assume m <= n;

          then

           A8: ||.((seq1 . n) - ( lim seq1)).|| < r by A7;

          ( - ( lim seq1)) = (( - 1) * ( lim seq1)) by RLVECT_1: 16

          .= (( - 1) * s) by SUBTH0

          .= ( - s) by RLVECT_1: 16;

          then ((seq1 . n) - ( lim seq1)) = ((seq . n) - s) by SUBTH0;

          hence ||.((seq . n) - s).|| < r by A8, SUBTH0;

        end;

        hence seq is convergent;

      end;

      hence thesis by LOPBAN_1:def 15;

    end;

    theorem :: NORMSP_3:48

    for V be RealNormSpace, V1 be SubRealNormSpace of V, CV1 be Subset of V st V1 is complete & CV1 = the carrier of V1 holds CV1 is closed

    proof

      let V be RealNormSpace, V1 be SubRealNormSpace of V, CV1 be Subset of V;

      assume

       A1: V1 is complete & CV1 = the carrier of V1;

      for s1 be sequence of V st ( rng s1) c= CV1 & s1 is convergent holds ( lim s1) in CV1

      proof

        let s1 be sequence of V;

        assume

         A2: ( rng s1) c= CV1 & s1 is convergent;

        then

        reconsider s2 = s1 as sequence of V1 by A1, FUNCT_2: 6;

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

        proof

          let s be Real;

          assume 0 < s;

          then

          consider n be Nat such that

           A3: for m be Nat st n <= m holds ||.((s1 . m) - (s1 . n)).|| < s by A2, LOPBAN_3: 4;

          take n;

          let m be Nat;

          assume n <= m;

          then

           A4: ||.((s1 . m) - (s1 . n)).|| < s by A3;

          ( - (s1 . n)) = (( - 1) * (s1 . n)) by RLVECT_1: 16

          .= (( - 1) * (s2 . n)) by SUBTH0

          .= ( - (s2 . n)) by RLVECT_1: 16;

          then ((s1 . m) - (s1 . n)) = ((s2 . m) - (s2 . n)) by SUBTH0;

          hence ||.((s2 . m) - (s2 . n)).|| < s by A4, SUBTH0;

        end;

        then

         A6: s2 is convergent by A1, LOPBAN_1:def 15, LOPBAN_3: 5;

        the carrier of V1 c= the carrier of V by DUALSP01:def 16;

        then

        reconsider s0 = ( lim s2) as Point of V;

        for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((s1 . n) - s0).|| < r

        proof

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

           A7: for n be Nat st m <= n holds ||.((s2 . n) - ( lim s2)).|| < r by A6, NORMSP_1:def 7;

          take m;

          let n be Nat;

          assume m <= n;

          then

           A8: ||.((s2 . n) - ( lim s2)).|| < r by A7;

          ( - ( lim s2)) = (( - 1) * ( lim s2)) by RLVECT_1: 16

          .= (( - 1) * s0) by SUBTH0

          .= ( - s0) by RLVECT_1: 16;

          then ((s2 . n) - ( lim s2)) = ((s1 . n) - s0) by SUBTH0;

          hence ||.((s1 . n) - s0).|| < r by A8, SUBTH0;

        end;

        then ( lim s1) = s0 by A2, NORMSP_1:def 7;

        hence ( lim s1) in CV1 by A1;

      end;

      hence thesis;

    end;

    theorem :: NORMSP_3:49

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

    proof

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

      assume

       A1: M is linearly-closed & M is closed;

      then the carrier of ( NLin M) = M by LCL1;

      hence thesis by A1, LM76A;

    end;

    begin

    definition

      let X be RealLinearSpace, Y be Subspace of X;

      :: original: RLSp2RVSp

      redefine

      func RLSp2RVSp Y -> Subspace of ( RLSp2RVSp X) ;

      correctness

      proof

        set V = ( RLSp2RVSp X);

        set W = ( RLSp2RVSp Y);

        

         A1: the carrier of W c= the carrier of V by RLSUB_1:def 2;

        

         A2: ( 0. W) = ( 0. Y)

        .= ( 0. X) by RLSUB_1:def 2

        .= ( 0. V);

        

         A3: the addF of W = (the addF of V || the carrier of W) by RLSUB_1:def 2;

        the lmult of W = (the lmult of V | [: REAL , the carrier of W:]) by RLSUB_1:def 2;

        hence thesis by A1, A2, A3, VECTSP_4:def 2;

      end;

    end

    definition

      let X be RealLinearSpace, Y be Subspace of X;

      :: NORMSP_3:def12

      func VectQuot (X,Y) -> RealLinearSpace equals ( RVSp2RLSp ( VectQuot (( RLSp2RVSp X),( RLSp2RVSp Y))));

      correctness ;

    end

    theorem :: NORMSP_3:50

    for X be RealLinearSpace, v be Element of X, a be Real, v1 be Element of ( RLSp2RVSp X), a1 be Element of F_Real st v = v1 & a = a1 holds (a * v) = (a1 * v1);

    theorem :: NORMSP_3:51

    for X be VectSp of F_Real , v be Element of X, a be Element of F_Real , v1 be Element of ( RVSp2RLSp X), a1 be Real st v = v1 & a = a1 holds (a * v) = (a1 * v1);

    theorem :: NORMSP_3:52

    

     LMQ03: for X be RealLinearSpace, Y be Subspace of X, v be Element of X, v1 be Element of ( RLSp2RVSp X) st v = v1 holds (v + Y) = (v1 + ( RLSp2RVSp Y))

    proof

      let X be RealLinearSpace, Y be Subspace of X, v be Element of X, v1 be Element of ( RLSp2RVSp X);

      set V = ( RLSp2RVSp X);

      set W = ( RLSp2RVSp Y);

      assume

       A1: v = v1;

      for x be object holds x in (v + Y) iff x in (v1 + W)

      proof

        let x be object;

        hereby

          assume x in (v + Y);

          then

          consider y be Point of X such that

           A2: x = (v + y) & y in Y;

          reconsider y1 = y as Point of V;

          

           A3: y1 in W by A2;

          (v + y) = (v1 + y1) by A1;

          hence x in (v1 + W) by A2, A3;

        end;

        assume x in (v1 + W);

        then

        consider y1 be Element of V such that

         A4: x = (v1 + y1) & y1 in W;

        reconsider y = y1 as Point of X;

        

         A5: y in Y by A4;

        (v + y) = (v1 + y1) by A1;

        hence x in (v + Y) by A4, A5;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: NORMSP_3:53

    

     LMQ04: for X be RealLinearSpace, Y be Subspace of X holds for x be object holds x is Coset of Y iff x is Coset of ( RLSp2RVSp Y)

    proof

      let X be RealLinearSpace, Y be Subspace of X;

      let x be object;

      hereby

        assume x is Coset of Y;

        then

        consider v be Element of X such that

         A1: x = (v + Y) by RLSUB_1:def 6;

        reconsider v1 = v as Element of ( RLSp2RVSp X);

        x = (v1 + ( RLSp2RVSp Y)) by A1, LMQ03;

        hence x is Coset of ( RLSp2RVSp Y) by VECTSP_4:def 6;

      end;

      assume x is Coset of ( RLSp2RVSp Y);

      then

      consider v1 be Element of ( RLSp2RVSp X) such that

       A2: x = (v1 + ( RLSp2RVSp Y)) by VECTSP_4:def 6;

      reconsider v = v1 as Element of X;

      x = (v + Y) by A2, LMQ03;

      hence x is Coset of Y by RLSUB_1:def 6;

    end;

    definition

      let X be RealLinearSpace, Y be Subspace of X;

      :: NORMSP_3:def13

      func CosetSet (X,Y) -> non empty Subset-Family of X equals the set of all A where A be Coset of Y;

      correctness

      proof

        set C = the set of all A where A be Coset of Y;

        

         A1: C c= ( bool the carrier of X)

        proof

          let x be object;

          assume x in C;

          then ex A be Coset of Y st A = x;

          hence thesis;

        end;

        the carrier of Y is Coset of Y by RLSUB_1: 74;

        then the carrier of Y in C;

        hence thesis by A1;

      end;

    end

    definition

      let V be RealLinearSpace, W be Subspace of V;

      :: NORMSP_3:def14

      func zeroCoset (V,W) -> Element of ( CosetSet (V,W)) equals the carrier of W;

      coherence

      proof

        the carrier of W = (( 0. V) + W) by RLSUB_1: 44;

        then the carrier of W is Coset of W by RLSUB_1:def 6;

        then the carrier of W in ( CosetSet (V,W));

        hence thesis;

      end;

    end

    theorem :: NORMSP_3:54

    

     LMQ05: for X be RealLinearSpace, Y be Subspace of X holds ( CosetSet (X,Y)) = ( CosetSet (( RLSp2RVSp X),( RLSp2RVSp Y)))

    proof

      let X be RealLinearSpace, Y be Subspace of X;

      for x be object holds x in ( CosetSet (X,Y)) iff x in ( CosetSet (( RLSp2RVSp X),( RLSp2RVSp Y)))

      proof

        let x be object;

        hereby

          assume x in ( CosetSet (X,Y));

          then

          consider A be Coset of Y such that

           A1: x = A;

          x is Coset of ( RLSp2RVSp Y) by A1, LMQ04;

          hence x in ( CosetSet (( RLSp2RVSp X),( RLSp2RVSp Y)));

        end;

        assume x in ( CosetSet (( RLSp2RVSp X),( RLSp2RVSp Y)));

        then

        consider B be Coset of ( RLSp2RVSp Y) such that

         A2: x = B;

        x is Coset of Y by A2, LMQ04;

        hence x in ( CosetSet (X,Y));

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: NORMSP_3:55

    

     LMQ06: for V be RealLinearSpace, W be Subspace of V holds the carrier of ( VectQuot (V,W)) = ( CosetSet (V,W))

    proof

      let V be RealLinearSpace, W be Subspace of V;

      set X = ( RLSp2RVSp V);

      set Y = ( RLSp2RVSp W);

      

      thus the carrier of ( VectQuot (V,W)) = ( CosetSet (X,Y)) by VECTSP10:def 6

      .= ( CosetSet (V,W)) by LMQ05;

    end;

    theorem :: NORMSP_3:56

    

     LMQ07: for V be RealLinearSpace, W be Subspace of V holds for x be object holds x is Point of ( VectQuot (V,W)) iff ex v be Point of V st x = (v + W)

    proof

      let V be RealLinearSpace, W be Subspace of V;

      let x be object;

      

       A1: x in the carrier of ( VectQuot (V,W)) iff x in ( CosetSet (V,W)) by LMQ06;

      (ex A be Coset of W st x = A) iff ex v be Point of V st x = (v + W)

      proof

        thus (ex A be Coset of W st x = A) implies ex v be Point of V st x = (v + W) by RLSUB_1:def 6;

        assume ex v be Point of V st x = (v + W);

        then x is Coset of W by RLSUB_1:def 6;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: NORMSP_3:57

    

     LMQ08: for V be RealLinearSpace, W be Subspace of V holds ( 0. ( VectQuot (V,W))) = ( zeroCoset (V,W))

    proof

      let V be RealLinearSpace, W be Subspace of V;

      set X = ( RLSp2RVSp V);

      set Y = ( RLSp2RVSp W);

      

      thus ( 0. ( VectQuot (V,W))) = ( 0. ( VectQuot (X,Y)))

      .= ( zeroCoset (X,Y)) by VECTSP10:def 6

      .= ( zeroCoset (V,W));

    end;

    theorem :: NORMSP_3:58

    

     LMQ09: for V be RealLinearSpace, W be Subspace of V holds for A be VECTOR of ( VectQuot (V,W)), v be VECTOR of V, a be Real st A = (v + W) holds (a * A) = ((a * v) + W)

    proof

      let V be RealLinearSpace, W be Subspace of V;

      set X = ( RLSp2RVSp V);

      set Y = ( RLSp2RVSp W);

      let A be VECTOR of ( VectQuot (V,W)), v be VECTOR of V, a be Real;

      assume

       A1: A = (v + W);

      reconsider v1 = v as Vector of X;

      reconsider A1 = A as Vector of ( VectQuot (X,Y));

      reconsider a1 = a as Element of F_Real by XREAL_0:def 1;

      

       A2: A1 = (v1 + Y) by A1, LMQ03;

      

      thus (a * A) = (a1 * A1)

      .= ((a1 * v1) + Y) by A2, VECTSP10: 25

      .= ((a * v) + W) by LMQ03;

    end;

    theorem :: NORMSP_3:59

    

     LMQ10: for V be RealLinearSpace, W be Subspace of V holds for A be VECTOR of ( VectQuot (V,W)), v be VECTOR of V, a be Real st A = (v + W) holds ( - A) = (( - v) + W)

    proof

      let V be RealLinearSpace, W be Subspace of V;

      let A be VECTOR of ( VectQuot (V,W)), v be VECTOR of V, a be Real;

      assume

       A1: A = (v + W);

      

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

      .= ((( - 1) * v) + W) by A1, LMQ09

      .= (( - v) + W) by RLVECT_1: 16;

    end;

    theorem :: NORMSP_3:60

    

     LMQ11: for V be RealLinearSpace, W be Subspace of V holds for A1,A2 be VECTOR of ( VectQuot (V,W)), v1,v2 be VECTOR of V st A1 = (v1 + W) & A2 = (v2 + W) holds (A1 + A2) = ((v1 + v2) + W)

    proof

      let V be RealLinearSpace, W be Subspace of V;

      set X = ( RLSp2RVSp V);

      set Y = ( RLSp2RVSp W);

      let A1,A2 be VECTOR of ( VectQuot (V,W)), v1,v2 be VECTOR of V;

      assume

       A1: A1 = (v1 + W) & A2 = (v2 + W);

      reconsider x1 = v1, x2 = v2 as Vector of X;

      reconsider B1 = A1, B2 = A2 as Vector of ( VectQuot (X,Y));

      

       A2: B1 = (x1 + Y) & B2 = (x2 + Y) by A1, LMQ03;

      

      thus (A1 + A2) = (B1 + B2)

      .= ((x1 + x2) + Y) by A2, VECTSP10: 26

      .= ((v1 + v2) + W) by LMQ03;

    end;

    theorem :: NORMSP_3:61

    for V be RealLinearSpace, W be Subspace of V holds for A1,A2 be VECTOR of ( VectQuot (V,W)), v1,v2 be VECTOR of V st A1 = (v1 + W) & A2 = (v2 + W) holds (A1 - A2) = ((v1 - v2) + W)

    proof

      let V be RealLinearSpace, W be Subspace of V;

      let A1,A2 be VECTOR of ( VectQuot (V,W)), v1,v2 be VECTOR of V;

      assume

       A1: A1 = (v1 + W) & A2 = (v2 + W);

      then ( - A2) = (( - v2) + W) by LMQ10;

      hence (A1 - A2) = ((v1 - v2) + W) by A1, LMQ11;

    end;

    theorem :: NORMSP_3:62

    

     LMQ13: for V be RealLinearSpace, W be Subspace of V holds ( 0. ( VectQuot (V,W))) = the carrier of W & ( 0. ( VectQuot (V,W))) = (( 0. V) + W)

    proof

      let V be RealLinearSpace, W be Subspace of V;

      

      thus ( 0. ( VectQuot (V,W))) = ( zeroCoset (V,W)) by LMQ08

      .= the carrier of W;

      hence ( 0. ( VectQuot (V,W))) = (( 0. V) + W) by RLSUB_1: 44;

    end;

    theorem :: NORMSP_3:63

    

     LMQ20: for V be RealLinearSpace, W be Subspace of V holds ex QL be LinearOperator of V, ( VectQuot (V,W)) st QL is onto & for v be VECTOR of V holds (QL . v) = (v + W)

    proof

      let V be RealLinearSpace, W be Subspace of V;

      defpred P[ VECTOR of V, object] means $2 = ($1 + W);

      

       A1: for x be Element of the carrier of V holds ex y be Element of the carrier of ( VectQuot (V,W)) st P[x, y]

      proof

        let x be Element of the carrier of V;

        reconsider v = (x + W) as Point of ( VectQuot (V,W)) by LMQ07;

        take v;

        thus thesis;

      end;

      consider QL be Function of the carrier of V, ( VectQuot (V,W)) such that

       A2: for x be Element of V holds P[x, (QL . x)] from FUNCT_2:sch 3( A1);

      

       A3: for v,w be Element of V holds (QL . (v + w)) = ((QL . v) + (QL . w))

      proof

        let v,w be Element of V;

        

         A4: (QL . v) = (v + W) by A2;

        

         A5: (QL . w) = (w + W) by A2;

        

        thus (QL . (v + w)) = ((v + w) + W) by A2

        .= ((QL . v) + (QL . w)) by A4, A5, LMQ11;

      end;

      for v be VECTOR of V, r be Real holds (QL . (r * v)) = (r * (QL . v))

      proof

        let v be VECTOR of V, r be Real;

        

         A6: (QL . v) = (v + W) by A2;

        

        thus (QL . (r * v)) = ((r * v) + W) by A2

        .= (r * (QL . v)) by A6, LMQ09;

      end;

      then QL is additive homogeneous by A3, LOPBAN_1:def 5;

      then

      reconsider QL as LinearOperator of V, ( VectQuot (V,W));

      take QL;

      for v be object st v in the carrier of ( VectQuot (V,W)) holds ex s be object st s in the carrier of V & v = (QL . s)

      proof

        let v be object;

        assume v in the carrier of ( VectQuot (V,W));

        then

        reconsider v1 = v as Point of ( VectQuot (V,W));

        consider s be VECTOR of V such that

         A7: v1 = (s + W) by LMQ07;

        take s;

        thus s in the carrier of V;

        thus v = (QL . s) by A2, A7;

      end;

      hence thesis by A2, FUNCT_2: 10;

    end;

    definition

      let V be RealLinearSpace, W be Subspace of V;

      :: NORMSP_3:def15

      func InducedSur (V,W) -> LinearOperator of V, ( VectQuot (V,W)) means

      : defDQuot: it is onto & for v be VECTOR of V holds (it . v) = (v + W);

      existence by LMQ20;

      uniqueness

      proof

        let QL1,QL2 be LinearOperator of V, ( VectQuot (V,W));

        assume

         A1: QL1 is onto & for v be VECTOR of V holds (QL1 . v) = (v + W);

        assume

         A2: QL2 is onto & for v be VECTOR of V holds (QL2 . v) = (v + W);

        now

          let v be VECTOR of V;

          

          thus (QL1 . v) = (v + W) by A1

          .= (QL2 . v) by A2;

        end;

        hence QL1 = QL2;

      end;

    end

    theorem :: NORMSP_3:64

    

     LMQ21: for V,W be RealLinearSpace, L be LinearOperator of V, W holds ex QL be LinearOperator of ( VectQuot (V,( Ker L))), ( Im L) st QL is isomorphism & for z be Point of ( VectQuot (V,( Ker L))), v be VECTOR of V st z = (v + ( Ker L)) holds (QL . z) = (L . v)

    proof

      let V,W be RealLinearSpace, L be LinearOperator of V, W;

      

       A1: the carrier of ( Im L) = ( rng L) by IMX2, LCL1;

      

       A2: the carrier of ( Ker L) = (L " {( 0. W)}) by KLXY1, LCL1;

      defpred P[ object, object] means ex v be VECTOR of V st $1 = (v + ( Ker L)) & $2 = (L . v);

      

       A3: for x be Element of the carrier of ( VectQuot (V,( Ker L))) holds ex y be Element of the carrier of ( Im L) st P[x, y]

      proof

        let x be Element of the carrier of ( VectQuot (V,( Ker L)));

        consider v be Point of V such that

         A4: x = (v + ( Ker L)) by LMQ07;

        reconsider y = (L . v) as Element of the carrier of ( Im L) by A1, FUNCT_2: 4;

        take y;

        thus thesis by A4;

      end;

      consider QL be Function of the carrier of ( VectQuot (V,( Ker L))), the carrier of ( Im L) such that

       A5: for x be Element of ( VectQuot (V,( Ker L))) holds P[x, (QL . x)] from FUNCT_2:sch 3( A3);

      

       A6: for z be Point of ( VectQuot (V,( Ker L))), v be VECTOR of V st z = (v + ( Ker L)) holds (QL . z) = (L . v)

      proof

        let z be Point of ( VectQuot (V,( Ker L))), v be VECTOR of V;

        assume

         A7: z = (v + ( Ker L));

        consider w be VECTOR of V such that

         A8: z = (w + ( Ker L)) & (QL . z) = (L . w) by A5;

        consider v1 be Point of V such that

         A9: v1 in ( Ker L) & w = (v + v1) by A7, A8, RLSUB_1: 54, RLSUB_1: 63;

        (w - v) = (v1 + (v - v)) by A9, RLVECT_1: 28

        .= (v1 + ( 0. V)) by RLVECT_1: 15

        .= v1 by RLVECT_1: 4;

        then

         A10: (w - v) in the carrier of V & (L . (w - v)) in {( 0. W)} by A2, A9, FUNCT_2: 38;

        (L . (w - v)) = (L . (w + (( - 1) * v))) by RLVECT_1: 16

        .= ((L . w) + (L . (( - 1) * v))) by VECTSP_1:def 20

        .= ((L . w) + (( - 1) * (L . v))) by LOPBAN_1:def 5

        .= ((L . w) + ( - (L . v))) by RLVECT_1: 16;

        then ((L . w) - (L . v)) = ( 0. W) by A10, TARSKI:def 1;

        

        then (L . v) = (((L . w) - (L . v)) + (L . v)) by RLVECT_1: 4

        .= ((L . w) - ((L . v) - (L . v))) by RLVECT_1: 29

        .= ((L . w) - ( 0. W)) by RLVECT_1: 15

        .= (L . w) by RLVECT_1: 13;

        hence (QL . z) = (L . v) by A8;

      end;

      

       A11: for x1,x2 be object st x1 in the carrier of ( VectQuot (V,( Ker L))) & x2 in the carrier of ( VectQuot (V,( Ker L))) & (QL . x1) = (QL . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A12: x1 in the carrier of ( VectQuot (V,( Ker L))) & x2 in the carrier of ( VectQuot (V,( Ker L))) & (QL . x1) = (QL . x2);

        reconsider z1 = x1, z2 = x2 as Point of ( VectQuot (V,( Ker L))) by A12;

        consider v1 be VECTOR of V such that

         A13: z1 = (v1 + ( Ker L)) & (QL . x1) = (L . v1) by A5;

        consider v2 be VECTOR of V such that

         A14: z2 = (v2 + ( Ker L)) & (QL . x2) = (L . v2) by A5;

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

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

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

        .= (L . (v1 - v2)) by RLVECT_1: 16;

        then (L . (v1 - v2)) = ( 0. W) by A12, A13, A14, RLVECT_1: 15;

        then (L . (v1 - v2)) in {( 0. W)} by TARSKI:def 1;

        then

         A15: (v1 - v2) in ( Ker L) by A2, FUNCT_2: 38;

        ((v1 - v2) + v2) = (v1 - (v2 - v2)) by RLVECT_1: 29

        .= (v1 - ( 0. V)) by RLVECT_1: 15

        .= v1 by RLVECT_1: 13;

        then v1 in (v2 + ( Ker L)) by A15;

        hence thesis by A13, A14, RLSUB_1: 54;

      end;

      for v be object st v in the carrier of ( Im L) holds ex s be object st s in the carrier of ( VectQuot (V,( Ker L))) & v = (QL . s)

      proof

        let v be object;

        assume v in the carrier of ( Im L);

        then v in ( rng L) by IMX2, LCL1;

        then

        consider x be object such that

         A16: x in the carrier of V & (L . x) = v by FUNCT_2: 11;

        reconsider x as Point of V by A16;

        reconsider s = (x + ( Ker L)) as Point of ( VectQuot (V,( Ker L))) by LMQ07;

        take s;

        thus s in the carrier of ( VectQuot (V,( Ker L))) & v = (QL . s) by A6, A16;

      end;

      then

       A17: QL is onto by FUNCT_2: 10;

      

       A18: for v,w be Element of ( VectQuot (V,( Ker L))) holds (QL . (v + w)) = ((QL . v) + (QL . w))

      proof

        let v,w be Element of ( VectQuot (V,( Ker L)));

        consider x be Point of V such that

         A19: v = (x + ( Ker L)) by LMQ07;

        consider y be Point of V such that

         A20: w = (y + ( Ker L)) by LMQ07;

        

         A21: (v + w) = ((x + y) + ( Ker L)) by A19, A20, LMQ11;

        

         A22: (QL . v) = (L . x) by A6, A19;

        

         A23: (QL . w) = (L . y) by A6, A20;

        

        thus (QL . (v + w)) = (L . (x + y)) by A6, A21

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

        .= ((QL . v) + (QL . w)) by A22, A23, RLSUB_1: 13;

      end;

      for v be VECTOR of ( VectQuot (V,( Ker L))), r be Real holds (QL . (r * v)) = (r * (QL . v))

      proof

        let v be VECTOR of ( VectQuot (V,( Ker L))), r be Real;

        consider x be Point of V such that

         A24: v = (x + ( Ker L)) by LMQ07;

        (r * v) = ((r * x) + ( Ker L)) by A24, LMQ09;

        

        hence (QL . (r * v)) = (L . (r * x)) by A6

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

        .= (r * (QL . v)) by A6, A24, RLSUB_1: 14;

      end;

      then QL is additive homogeneous by A18, LOPBAN_1:def 5;

      then

      reconsider QL as LinearOperator of ( VectQuot (V,( Ker L))), ( Im L);

      take QL;

      thus QL is isomorphism by A11, A17, FUNCT_2: 19;

      thus thesis by A6;

    end;

    definition

      let V,W be RealLinearSpace, L be LinearOperator of V, W;

      :: NORMSP_3:def16

      func InducedBi (V,W,L) -> LinearOperator of ( VectQuot (V,( Ker L))), ( Im L) means

      : defQuotR: it is isomorphism & for z be Point of ( VectQuot (V,( Ker L))), v be VECTOR of V st z = (v + ( Ker L)) holds (it . z) = (L . v);

      existence by LMQ21;

      uniqueness

      proof

        let QL1,QL2 be LinearOperator of ( VectQuot (V,( Ker L))), ( Im L);

        assume

         A1: QL1 is isomorphism & for z be Point of ( VectQuot (V,( Ker L))), v be VECTOR of V st z = (v + ( Ker L)) holds (QL1 . z) = (L . v);

        assume

         A2: QL2 is isomorphism & for z be Point of ( VectQuot (V,( Ker L))), v be VECTOR of V st z = (v + ( Ker L)) holds (QL2 . z) = (L . v);

        now

          let z be VECTOR of ( VectQuot (V,( Ker L)));

          consider v be Point of V such that

           A3: z = (v + ( Ker L)) by LMQ07;

          

          thus (QL1 . z) = (L . v) by A1, A3

          .= (QL2 . z) by A2, A3;

        end;

        hence QL1 = QL2;

      end;

    end

    theorem :: NORMSP_3:65

    for V,W be RealLinearSpace, L be LinearOperator of V, W holds L = (( InducedBi (V,W,L)) * ( InducedSur (V,( Ker L))))

    proof

      let V,W be RealLinearSpace, L be LinearOperator of V, W;

      now

        let v be VECTOR of V;

        

         A1: ( dom ( InducedSur (V,( Ker L)))) = the carrier of V by FUNCT_2:def 1;

        reconsider z = (v + ( Ker L)) as Point of ( VectQuot (V,( Ker L))) by LMQ07;

        

        thus ((( InducedBi (V,W,L)) * ( InducedSur (V,( Ker L)))) . v) = (( InducedBi (V,W,L)) . (( InducedSur (V,( Ker L))) . v)) by A1, FUNCT_1: 13

        .= (( InducedBi (V,W,L)) . z) by defDQuot

        .= (L . v) by defQuotR;

      end;

      hence thesis;

    end;

    definition

      let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;

      :: NORMSP_3:def17

      func NormVSets (V,W,v) -> non empty Subset of REAL equals { ||.x.|| where x be VECTOR of V : x in (v + W) };

      correctness

      proof

        now

          let r be object;

          assume r in { ||.x.|| where x be VECTOR of V : x in (v + W) };

          then

          consider x be VECTOR of V such that

           A1: r = ||.x.|| & x in (v + W);

          thus r in REAL by A1;

        end;

        then

         A2: { ||.x.|| where x be VECTOR of V : x in (v + W) } c= REAL ;

        v in (v + W) by RLSUB_1: 43;

        then ||.v.|| in { ||.x.|| where x be VECTOR of V : x in (v + W) };

        hence thesis by A2;

      end;

    end

    

     LMQ231: for V be RealNormSpace, W be Subspace of V, v be VECTOR of V holds ( NormVSets (V,W,v)) is bounded_below

    proof

      let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;

      for r be ExtReal st r in ( NormVSets (V,W,v)) holds 0 <= r

      proof

        let r be ExtReal;

        assume r in ( NormVSets (V,W,v));

        then

        consider x be VECTOR of V such that

         A1: r = ||.x.|| & x in (v + W);

        thus thesis by A1;

      end;

      then 0 is LowerBound of ( NormVSets (V,W,v)) by XXREAL_2:def 2;

      hence ( NormVSets (V,W,v)) is bounded_below by XXREAL_2:def 9;

    end;

    registration

      let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;

      cluster ( NormVSets (V,W,v)) -> non empty bounded_below;

      correctness by LMQ231;

    end

    theorem :: NORMSP_3:66

    

     LMQ23: for V be RealNormSpace, W be Subspace of V, v be VECTOR of V holds 0 <= ( lower_bound ( NormVSets (V,W,v))) & ( lower_bound ( NormVSets (V,W,v))) <= ||.v.||

    proof

      let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;

      for r be ExtReal st r in ( NormVSets (V,W,v)) holds 0 <= r

      proof

        let r be ExtReal;

        assume r in ( NormVSets (V,W,v));

        then

        consider x be VECTOR of V such that

         A1: r = ||.x.|| & x in (v + W);

        thus thesis by A1;

      end;

      then 0 is LowerBound of ( NormVSets (V,W,v)) by XXREAL_2:def 2;

      hence 0 <= ( lower_bound ( NormVSets (V,W,v))) by XXREAL_2:def 4;

      v in (v + W) by RLSUB_1: 43;

      then

       A2: ||.v.|| in ( NormVSets (V,W,v));

      ( inf ( NormVSets (V,W,v))) is LowerBound of ( NormVSets (V,W,v)) by XXREAL_2:def 4;

      hence thesis by A2, XXREAL_2:def 2;

    end;

    definition

      let V be RealNormSpace, W be Subspace of V;

      :: NORMSP_3:def18

      func NormCoset (V,W) -> Function of ( CosetSet (V,W)), REAL means

      : DeNorm: for A be Element of ( CosetSet (V,W)) holds for v be VECTOR of V st A = (v + W) holds (it . A) = ( lower_bound ( NormVSets (V,W,v)));

      existence

      proof

        defpred P[ set, set] means for v be VECTOR of V st $1 = (v + W) holds $2 = ( lower_bound ( NormVSets (V,W,v)));

        set C = ( CosetSet (V,W));

         A1:

        now

          let A be Element of C;

          A in C;

          then

          consider A1 be Coset of W such that

           A2: A1 = A;

          consider v0 be VECTOR of V such that

           A3: A1 = (v0 + W) by RLSUB_1:def 6;

          reconsider r = ( lower_bound ( NormVSets (V,W,v0))) as Element of REAL by XREAL_0:def 1;

          take r;

          thus P[A, r] by A2, A3;

        end;

        consider f be Function of C, REAL such that

         A4: for A be Element of C holds P[A, (f . A)] from FUNCT_2:sch 3( A1);

        take f;

        let A be Element of C, v be VECTOR of V;

        assume A = (v + W);

        hence thesis by A4;

      end;

      uniqueness

      proof

        set C = ( CosetSet (V,W));

        let f1,f2 be Function of C, REAL such that

         A5: for A be Element of ( CosetSet (V,W)) holds for a be VECTOR of V st A = (a + W) holds (f1 . A) = ( lower_bound ( NormVSets (V,W,a))) and

         A6: for A be Element of ( CosetSet (V,W)) holds for a be VECTOR of V st A = (a + W) holds (f2 . A) = ( lower_bound ( NormVSets (V,W,a)));

        set C = ( CosetSet (V,W));

        now

          let A be Element of ( CosetSet (V,W));

          A in C;

          then

          consider A1 be Coset of W such that

           A7: A1 = A;

          consider a be VECTOR of V such that

           A8: A1 = (a + W) by RLSUB_1:def 6;

          

          thus (f1 . A) = ( lower_bound ( NormVSets (V,W,a))) by A5, A7, A8

          .= (f2 . A) by A6, A7, A8;

        end;

        hence thesis;

      end;

    end

    definition

      let X be RealNormSpace, Y be Subspace of X;

      assume

       A1: ex CY be Subset of X st CY = the carrier of Y & CY is closed;

      :: NORMSP_3:def19

      func NVectQuot (X,Y) -> strict RealNormSpace means

      : defQuotN: the RLSStruct of it = ( VectQuot (X,Y)) & the normF of it = ( NormCoset (X,Y));

      existence

      proof

        consider CY be Subset of X such that

         A2: CY = the carrier of Y & CY is closed by A1;

        set S = ( VectQuot (X,Y));

        

         A3: the carrier of S = ( CosetSet (X,Y)) by LMQ06;

        then

        reconsider NF = ( NormCoset (X,Y)) as Function of the carrier of S, REAL ;

        reconsider T = NORMSTR (# the carrier of S, ( 0. S), the addF of S, the Mult of S, NF #) as non empty NORMSTR;

        now

          let v,w be Element of T;

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

          

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

          .= (w1 + v1)

          .= (w + v);

        end;

        then

         A4: T is Abelian;

        now

          let u,v,w be Element of T;

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

          

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

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

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

        end;

        then

         A5: T is add-associative;

        now

          let v be Element of T;

          reconsider v1 = v as Element of S;

          

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

          .= v by RLVECT_1:def 4;

        end;

        then

         A6: T is right_zeroed;

        

         A7: T is right_complementable

        proof

          let v be Element of T;

          reconsider v1 = v as Element of S;

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

          reconsider w = w1 as Element of T;

          take w;

          

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

          .= ( 0. T) by RLVECT_1: 5;

        end;

        now

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

          reconsider v1 = v as Element of S;

          

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

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

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

        end;

        then

         A8: T is scalar-distributive;

        now

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

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

          

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

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

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

        end;

        then

         A9: T is vector-distributive;

        now

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

          reconsider v1 = v as Element of S;

          

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

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

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

        end;

        then

         A10: T is scalar-associative;

        now

          let v be Element of T;

          reconsider v1 = v as Element of S;

          

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

          .= v by RLVECT_1:def 8;

        end;

        then

         A11: T is scalar-unital;

        

         A13: ||.( 0. T).|| = ( lower_bound ( NormVSets (X,Y,( 0. X)))) by A3, DeNorm, LMQ13;

        then

         A14: ||.( 0. T).|| <= ||.( 0. X).|| by LMQ23;

        then

         A15: T is reflexive by A13, LMQ23;

        now

          let z be Element of T;

          assume

           A16: ||.z.|| = 0 ;

          reconsider z1 = z as Element of S;

          consider v be Point of X such that

           A17: z1 = (v + Y) by LMQ07;

          

           A18: 0 = ( lower_bound ( NormVSets (X,Y,v))) by A3, A16, A17, DeNorm;

          for e be Real st 0 < e holds ex w be VECTOR of X st w in CY & ||.(v - w).|| <= e

          proof

            let e be Real;

            set g = ( lower_bound ( NormVSets (X,Y,v)));

            assume 0 < e;

            then

            consider r be Real such that

             A19: r in ( NormVSets (X,Y,v)) & r < (g + e) by SEQ_4:def 2;

            consider x be VECTOR of X such that

             A20: r = ||.x.|| & x in (v + Y) by A19;

            consider u be Point of X such that

             A21: x = (v + u) & u in Y by A20;

            set w = ( - u);

            take w;

            w in Y by A21, RLSUB_1: 22;

            hence w in CY by A2;

            thus ||.(v - w).|| <= e by A18, A19, A20, A21, RLVECT_1: 17;

          end;

          then v in Y by A2, CLOSE1;

          then (v + Y) = the carrier of Y by RLSUB_1: 48;

          hence z = ( 0. T) by A17, LMQ13;

        end;

        then

         A22: T is discerning;

        now

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

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

          thus ||.(a * v).|| = ( |.a.| * ||.v.||)

          proof

            per cases ;

              suppose

               A23: a = 0 ;

              

              then ( 0. T) = (a * v1) by RLVECT_1: 10

              .= (a * v);

              hence thesis by A13, A14, A23, COMPLEX1: 44, LMQ23;

            end;

              suppose

               A24: not a = 0 ;

              then

               A25: 0 < |.a.| by COMPLEX1: 47;

              consider vv1 be Point of X such that

               A26: v1 = (vv1 + Y) by LMQ07;

              

               A27: ||.v.|| = ( lower_bound ( NormVSets (X,Y,vv1))) by A3, A26, DeNorm;

              (a * v) = (a * v1)

              .= ((a * vv1) + Y) by A26, LMQ09;

              then

               A29: ||.(a * v).|| = ( lower_bound ( NormVSets (X,Y,(a * vv1)))) by A3, DeNorm;

              for r be ExtReal st r in ( NormVSets (X,Y,(a * vv1))) holds ( |.a.| * ||.v.||) <= r

              proof

                let r be ExtReal;

                assume r in ( NormVSets (X,Y,(a * vv1)));

                then

                consider x be VECTOR of X such that

                 A30: r = ||.x.|| & x in ((a * vv1) + Y);

                consider y be VECTOR of X such that

                 A31: x = ((a * vv1) + y) & y in Y by A30;

                

                 A32: ((a * vv1) + y) = ((a * vv1) + (1 * y)) by RLVECT_1:def 8

                .= ((a * vv1) + ((a * (1 / a)) * y)) by A24, XCMPLX_1: 106

                .= ((a * vv1) + (a * ((1 / a) * y))) by RLVECT_1:def 7

                .= (a * (vv1 + ((1 / a) * y))) by RLVECT_1:def 5;

                

                 A33: ((1 / a) * y) in Y by A31, RLSUB_1: 21;

                

                 A34: ||.((a * vv1) + y).|| = ( |.a.| * ||.(vv1 + ((1 / a) * y)).||) by A32, NORMSP_1:def 1;

                (vv1 + ((1 / a) * y)) in (vv1 + Y) by A33;

                then ||.(vv1 + ((1 / a) * y)).|| in ( NormVSets (X,Y,vv1));

                then ||.v.|| <= ||.(vv1 + ((1 / a) * y)).|| by A27, SEQ_4:def 2;

                hence thesis by A25, A30, A31, A34, XREAL_1: 64;

              end;

              then ( |.a.| * ||.v.||) is LowerBound of ( NormVSets (X,Y,(a * vv1))) by XXREAL_2:def 2;

              then

               A36: ( |.a.| * ||.v.||) <= ||.(a * v).|| by A29, XXREAL_2:def 4;

              for r be ExtReal st r in ( NormVSets (X,Y,vv1)) holds ((1 / |.a.|) * ||.(a * v).||) <= r

              proof

                let r be ExtReal;

                assume r in ( NormVSets (X,Y,vv1));

                then

                consider x be VECTOR of X such that

                 A37: r = ||.x.|| & x in (vv1 + Y);

                consider y be VECTOR of X such that

                 A38: x = (vv1 + y) & y in Y by A37;

                

                 A39: (vv1 + y) = (1 * (vv1 + y)) by RLVECT_1:def 8

                .= (((1 / a) * a) * (vv1 + y)) by A24, XCMPLX_1: 106

                .= ((1 / a) * (a * (vv1 + y))) by RLVECT_1:def 7

                .= ((1 / a) * ((a * vv1) + (a * y))) by RLVECT_1:def 5;

                

                 A40: (a * y) in Y by A38, RLSUB_1: 21;

                

                 A41: ||.(vv1 + y).|| = ( |.(1 / a).| * ||.((a * vv1) + (a * y)).||) by A39, NORMSP_1:def 1;

                ((a * vv1) + (a * y)) in ((a * vv1) + Y) by A40;

                then ||.((a * vv1) + (a * y)).|| in ( NormVSets (X,Y,(a * vv1)));

                then

                 A42: ||.(a * v).|| <= ||.((a * vv1) + (a * y)).|| by A29, SEQ_4:def 2;

                 0 <= |.(1 / a).| by COMPLEX1: 46;

                then ( |.(1 / a).| * ||.(a * v).||) <= ( |.(1 / a).| * ||.((a * vv1) + (a * y)).||) by A42, XREAL_1: 64;

                hence thesis by A37, A38, A41, COMPLEX1: 80;

              end;

              then

               A43: ((1 / |.a.|) * ||.(a * v).||) is LowerBound of ( NormVSets (X,Y,vv1)) by XXREAL_2:def 2;

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

              then ( |.a.| * ((1 / |.a.|) * ||.(a * v).||)) <= ( |.a.| * ||.v.||) by A27, A43, XREAL_1: 64, XXREAL_2:def 4;

              then (( |.a.| * (1 / |.a.|)) * ||.(a * v).||) <= ( |.a.| * ||.v.||);

              then (1 * ||.(a * v).||) <= ( |.a.| * ||.v.||) by A25, XCMPLX_1: 106;

              hence ||.(a * v).|| = ( |.a.| * ||.v.||) by A36, XXREAL_0: 1;

            end;

          end;

          thus ||.(v + w).|| <= ( ||.v.|| + ||.w.||)

          proof

            consider vv1 be Point of X such that

             A44: v1 = (vv1 + Y) by LMQ07;

            

             A45: ||.v.|| = ( lower_bound ( NormVSets (X,Y,vv1))) by A3, A44, DeNorm;

            consider ww1 be Point of X such that

             A46: w1 = (ww1 + Y) by LMQ07;

            

             A47: ||.w.|| = ( lower_bound ( NormVSets (X,Y,ww1))) by A3, A46, DeNorm;

            (v + w) = (v1 + w1)

            .= ((vv1 + ww1) + Y) by A44, A46, LMQ11;

            then

             A49: ||.(v + w).|| = ( lower_bound ( NormVSets (X,Y,(vv1 + ww1)))) by A3, DeNorm;

            

             A50: for y1,y2 be Point of X st y1 in Y & y2 in Y holds ||.(v + w).|| <= ( ||.(vv1 + y1).|| + ||.(ww1 + y2).||)

            proof

              let y1,y2 be Point of X;

              assume y1 in Y & y2 in Y;

              then (y1 + y2) in Y by RLSUB_1: 20;

              then ((vv1 + ww1) + (y1 + y2)) in ((vv1 + ww1) + Y);

              then ||.((vv1 + ww1) + (y1 + y2)).|| in ( NormVSets (X,Y,(vv1 + ww1)));

              then

               A51: ( lower_bound ( NormVSets (X,Y,(vv1 + ww1)))) <= ||.((vv1 + ww1) + (y1 + y2)).|| by SEQ_4:def 2;

               ||.((vv1 + ww1) + (y1 + y2)).|| = ||.(((vv1 + ww1) + y1) + y2).|| by RLVECT_1:def 3

              .= ||.(((vv1 + y1) + ww1) + y2).|| by RLVECT_1:def 3

              .= ||.((vv1 + y1) + (ww1 + y2)).|| by RLVECT_1:def 3;

              then ||.((vv1 + ww1) + (y1 + y2)).|| <= ( ||.(vv1 + y1).|| + ||.(ww1 + y2).||) by NORMSP_1:def 1;

              hence thesis by A49, A51, XXREAL_0: 2;

            end;

            

             A52: for y1 be Point of X st y1 in Y holds ( ||.(v + w).|| - ||.w.||) <= ||.(vv1 + y1).||

            proof

              let y1 be Point of X;

              assume

               A53: y1 in Y;

               A54:

              now

                let y2 be Point of X;

                assume y2 in Y;

                then ( ||.(v + w).|| - ||.(vv1 + y1).||) <= (( ||.(vv1 + y1).|| + ||.(ww1 + y2).||) - ||.(vv1 + y1).||) by A50, A53, XREAL_1: 9;

                hence ( ||.(v + w).|| - ||.(vv1 + y1).||) <= ||.(ww1 + y2).||;

              end;

              for r be ExtReal st r in ( NormVSets (X,Y,ww1)) holds ( ||.(v + w).|| - ||.(vv1 + y1).||) <= r

              proof

                let r be ExtReal;

                assume r in ( NormVSets (X,Y,ww1));

                then

                consider x be VECTOR of X such that

                 A55: r = ||.x.|| & x in (ww1 + Y);

                consider y2 be VECTOR of X such that

                 A56: x = (ww1 + y2) & y2 in Y by A55;

                thus ( ||.(v + w).|| - ||.(vv1 + y1).||) <= r by A54, A55, A56;

              end;

              then ( ||.(v + w).|| - ||.(vv1 + y1).||) is LowerBound of ( NormVSets (X,Y,ww1)) by XXREAL_2:def 2;

              then (( ||.(v + w).|| - ||.(vv1 + y1).||) + ||.(vv1 + y1).||) <= ( ||.w.|| + ||.(vv1 + y1).||) by A47, XREAL_1: 6, XXREAL_2:def 4;

              then ( ||.(v + w).|| - ||.w.||) <= (( ||.w.|| + ||.(vv1 + y1).||) - ||.w.||) by XREAL_1: 9;

              hence ( ||.(v + w).|| - ||.w.||) <= ||.(vv1 + y1).||;

            end;

            for r be ExtReal st r in ( NormVSets (X,Y,vv1)) holds ( ||.(v + w).|| - ||.w.||) <= r

            proof

              let r be ExtReal;

              assume r in ( NormVSets (X,Y,vv1));

              then

              consider x be VECTOR of X such that

               A58: r = ||.x.|| & x in (vv1 + Y);

              consider y1 be VECTOR of X such that

               A59: x = (vv1 + y1) & y1 in Y by A58;

              thus thesis by A52, A58, A59;

            end;

            then ( ||.(v + w).|| - ||.w.||) is LowerBound of ( NormVSets (X,Y,vv1)) by XXREAL_2:def 2;

            then (( ||.(v + w).|| - ||.w.||) + ||.w.||) <= ( ||.v.|| + ||.w.||) by A45, XREAL_1: 6, XXREAL_2:def 4;

            hence thesis;

          end;

        end;

        then T is RealNormSpace-like;

        then

        reconsider T as strict RealNormSpace by A4, A5, A6, A7, A8, A9, A10, A11, A15, A22;

        take T;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: NORMSP_3:67

    for V,W be RealNormSpace, L be Lipschitzian LinearOperator of V, W holds ex QL be Lipschitzian LinearOperator of ( NVectQuot (V,( Ker L))), ( Im L), PQL be Point of ( R_NormSpace_of_BoundedLinearOperators (( NVectQuot (V,( Ker L))),( Im L))), PL be Point of ( R_NormSpace_of_BoundedLinearOperators (V,W)) st QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & for z be Point of ( NVectQuot (V,( Ker L))), v be VECTOR of V st z = (v + ( Ker L)) holds (QL . z) = (L . v)

    proof

      let V,W be RealNormSpace, L be Lipschitzian LinearOperator of V, W;

      

       A1: the carrier of ( Ker L) = (L " {( 0. W)}) & (L " {( 0. W)}) is closed by KERCL01, KLXY1, LCL1, LOPBAN_7: 6;

      reconsider V1 = V as RealLinearSpace;

      reconsider W1 = W as RealLinearSpace;

      reconsider L1 = L as LinearOperator of V1, W1;

      

       A2: the RLSStruct of ( NVectQuot (V,( Ker L))) = ( VectQuot (V,( Ker L))) & the normF of ( NVectQuot (V,( Ker L))) = ( NormCoset (V,( Ker L))) by A1, defQuotN;

      

       A3: the carrier of ( VectQuot (V,( Ker L))) = ( CosetSet (V,( Ker L))) by LMQ06;

      consider QL1 be LinearOperator of ( VectQuot (V1,( Ker L1))), ( Im L1) such that

       A4: QL1 is isomorphism & for z be Point of ( VectQuot (V1,( Ker L1))), v be VECTOR of V1 st z = (v + ( Ker L1)) holds (QL1 . z) = (L1 . v) by LMQ21;

      reconsider KL1 = ( Ker L1) as Subspace of V;

      

       A5: the RLSStruct of ( NVectQuot (V,( Ker L))) = ( VectQuot (V,KL1)) by A1, defQuotN;

      reconsider QL = QL1 as Function of ( NVectQuot (V,( Ker L))), ( Im L) by A5;

      

       A6: for v,w be Element of ( NVectQuot (V,( Ker L))) holds (QL . (v + w)) = ((QL . v) + (QL . w))

      proof

        let v,w be Element of ( NVectQuot (V,( Ker L)));

        reconsider v1 = v, w1 = w as Element of ( VectQuot (V1,( Ker L1))) by A5;

        

        thus (QL . (v + w)) = (QL1 . (v1 + w1)) by A5

        .= ((QL1 . v1) + (QL1 . w1)) by VECTSP_1:def 20

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

      end;

      for v be VECTOR of ( NVectQuot (V,( Ker L))), r be Real holds (QL . (r * v)) = (r * (QL . v))

      proof

        let v be VECTOR of ( NVectQuot (V,( Ker L))), r be Real;

        reconsider v1 = v as Element of ( VectQuot (V1,( Ker L1))) by A5;

        

        thus (QL . (r * v)) = (QL1 . (r * v1)) by A5

        .= (r * (QL1 . v1)) by LOPBAN_1:def 5

        .= (r * (QL . v));

      end;

      then QL is additive homogeneous by A6, LOPBAN_1:def 5;

      then

      reconsider QL as LinearOperator of ( NVectQuot (V,( Ker L))), ( Im L);

      

       A7: ( R_NormSpace_of_BoundedLinearOperators (V,W)) = NORMSTR (# ( BoundedLinearOperators (V,W)), ( Zero_ (( BoundedLinearOperators (V,W)),( R_VectorSpace_of_LinearOperators (V,W)))), ( Add_ (( BoundedLinearOperators (V,W)),( R_VectorSpace_of_LinearOperators (V,W)))), ( Mult_ (( BoundedLinearOperators (V,W)),( R_VectorSpace_of_LinearOperators (V,W)))), ( BoundedLinearOperatorsNorm (V,W)) #) by LOPBAN_1:def 14;

      reconsider PL = L as Point of ( R_NormSpace_of_BoundedLinearOperators (V,W)) by A7, LOPBAN_1:def 9;

      

       A8: for v be Point of ( NVectQuot (V,( Ker L))) holds ||.(QL . v).|| <= ( ||.PL.|| * ||.v.||)

      proof

        let v be Point of ( NVectQuot (V,( Ker L)));

        reconsider v1 = v as Element of ( VectQuot (V,( Ker L))) by A5;

        consider vv1 be Point of V such that

         A9: v1 = (vv1 + ( Ker L)) by LMQ07;

        

         A10: ||.v.|| = (( NormCoset (V,( Ker L))) . v1) by A1, defQuotN

        .= ( lower_bound ( NormVSets (V,( Ker L),vv1))) by A3, A9, DeNorm;

        per cases ;

          suppose ||.PL.|| = 0 ;

          then PL = ( 0. ( R_NormSpace_of_BoundedLinearOperators (V,W))) by NORMSP_0:def 5;

          then

           A11: (the carrier of V --> ( 0. W)) = L by LOPBAN_1: 31;

          (QL . v) = (L . vv1) by A4, A9

          .= ( 0. W) by A11, FUNCOP_1: 7;

          then ||.(QL . v).|| = ||.( 0. W).|| by SUBTH0;

          hence ||.(QL . v).|| <= ( ||.PL.|| * ||.v.||);

        end;

          suppose

           A12: ||.PL.|| <> 0 ;

          set a = ||.PL.||;

          

           A13: for y be VECTOR of V st y in ( Ker L) holds ((1 / a) * ||.(QL . v).||) <= ||.(vv1 + y).||

          proof

            let y be VECTOR of V;

            assume y in ( Ker L);

            then y in (L " {( 0. W)}) by KLXY1, LCL1;

            then

             A14: y in the carrier of V & (L . y) in {( 0. W)} by FUNCT_2: 38;

            

             A15: (QL . v) = (L . vv1) by A4, A9

            .= ((L . vv1) + ( 0. W)) by RLVECT_1: 4

            .= ((L . vv1) + (L . y)) by A14, TARSKI:def 1

            .= (L . (vv1 + y)) by VECTSP_1:def 20;

            ((1 / a) * ||.(L . (vv1 + y)).||) <= ((1 / a) * ( ||.PL.|| * ||.(vv1 + y).||)) by LOPBAN_1: 32, XREAL_1: 64;

            then ((1 / a) * ||.(L . (vv1 + y)).||) <= (((1 / a) * ||.PL.||) * ||.(vv1 + y).||);

            then ((1 / a) * ||.(L . (vv1 + y)).||) <= (1 * ||.(vv1 + y).||) by A12, XCMPLX_1: 106;

            hence thesis by A15, SUBTH0;

          end;

          for r be ExtReal st r in ( NormVSets (V,( Ker L),vv1)) holds ((1 / a) * ||.(QL . v).||) <= r

          proof

            let r be ExtReal;

            assume r in ( NormVSets (V,( Ker L),vv1));

            then

            consider x be VECTOR of V such that

             A16: r = ||.x.|| & x in (vv1 + ( Ker L));

            consider y be VECTOR of V such that

             A17: x = (vv1 + y) & y in ( Ker L) by A16;

            thus thesis by A13, A16, A17;

          end;

          then

           A18: ((1 / a) * ||.(QL . v).||) is LowerBound of ( NormVSets (V,( Ker L),vv1)) by XXREAL_2:def 2;

          (a * ((1 / a) * ||.(QL . v).||)) <= (a * ||.v.||) by A10, A18, XREAL_1: 64, XXREAL_2:def 4;

          then ((a * (1 / a)) * ||.(QL . v).||) <= (a * ||.v.||);

          then (1 * ||.(QL . v).||) <= (a * ||.v.||) by A12, XCMPLX_1: 106;

          hence ||.(QL . v).|| <= ( ||.PL.|| * ||.v.||);

        end;

      end;

      reconsider QL as Lipschitzian LinearOperator of ( NVectQuot (V,( Ker L))), ( Im L) by A8, LOPBAN_1:def 8;

      take QL;

      

       A19: ( R_NormSpace_of_BoundedLinearOperators (( NVectQuot (V,( Ker L))),( Im L))) = NORMSTR (# ( BoundedLinearOperators (( NVectQuot (V,( Ker L))),( Im L))), ( Zero_ (( BoundedLinearOperators (( NVectQuot (V,( Ker L))),( Im L))),( R_VectorSpace_of_LinearOperators (( NVectQuot (V,( Ker L))),( Im L))))), ( Add_ (( BoundedLinearOperators (( NVectQuot (V,( Ker L))),( Im L))),( R_VectorSpace_of_LinearOperators (( NVectQuot (V,( Ker L))),( Im L))))), ( Mult_ (( BoundedLinearOperators (( NVectQuot (V,( Ker L))),( Im L))),( R_VectorSpace_of_LinearOperators (( NVectQuot (V,( Ker L))),( Im L))))), ( BoundedLinearOperatorsNorm (( NVectQuot (V,( Ker L))),( Im L))) #) by LOPBAN_1:def 14;

      then

      reconsider PQL = QL as Point of ( R_NormSpace_of_BoundedLinearOperators (( NVectQuot (V,( Ker L))),( Im L))) by LOPBAN_1:def 9;

      

       A20: ( PreNorms QL) = { ||.(QL . t).|| where t be VECTOR of ( NVectQuot (V,( Ker L))) : ||.t.|| <= 1 } by LOPBAN_1:def 12;

      now

        let r be Real;

        assume r in ( PreNorms QL);

        then

        consider v be VECTOR of ( NVectQuot (V,( Ker L))) such that

         A21: r = ||.(QL . v).|| and

         A22: ||.v.|| <= 1 by A20;

        

         A23: ||.(QL . v).|| <= ( ||.PL.|| * ||.v.||) by A8;

        ( ||.PL.|| * ||.v.||) <= ( ||.PL.|| * 1) by A22, XREAL_1: 64;

        hence r <= ||.PL.|| by A21, A23, XXREAL_0: 2;

      end;

      then ( upper_bound ( PreNorms QL)) <= ||.PL.|| by SEQ_4: 45;

      then

       A24: ||.PQL.|| <= ||.PL.|| by A19, LOPBAN_1: 30;

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

      then

       A26: ||.PL.|| = ( upper_bound ( PreNorms L)) by LOPBAN_1: 30;

      

       A27: ( PreNorms L) is non empty bounded_above by LOPBAN_1: 27;

      

       A28: ( PreNorms L) = { ||.(L . t).|| where t be VECTOR of V : ||.t.|| <= 1 } by LOPBAN_1:def 12;

      now

        let s be Real;

        assume 0 < s;

        then

        consider p be Real such that

         A29: p in ( PreNorms L) & ( ||.PL.|| - s) < p by A26, A27, SEQ_4:def 1;

        consider vv1 be VECTOR of V such that

         A30: p = ||.(L . vv1).|| and

         A31: ||.vv1.|| <= 1 by A28, A29;

        

         A32: ( lower_bound ( NormVSets (V,( Ker L),vv1))) <= ||.vv1.|| by LMQ23;

        reconsider v = (vv1 + ( Ker L)) as Point of ( NVectQuot (V,( Ker L))) by A2, LMQ07;

         ||.v.|| = ( lower_bound ( NormVSets (V,( Ker L),vv1))) by A2, DeNorm;

        then

         A33: ||.v.|| <= 1 by A31, A32, XXREAL_0: 2;

        (QL . v) = (L . vv1) by A4, A5;

        then

         A34: ||.(QL . v).|| = ||.(L . vv1).|| by SUBTH0;

        

         A35: ||.(QL . v).|| <= ( ||.PQL.|| * ||.v.||) by LOPBAN_1: 32;

        ( ||.PQL.|| * ||.v.||) <= ( ||.PQL.|| * 1) by A33, XREAL_1: 64;

        then ||.(QL . v).|| <= ||.PQL.|| by A35, XXREAL_0: 2;

        then ( ||.PL.|| - s) <= ||.PQL.|| by A29, A30, A34, XXREAL_0: 2;

        then (( ||.PL.|| - s) + s) <= ( ||.PQL.|| + s) by XREAL_1: 6;

        hence ||.PL.|| <= ( ||.PQL.|| + (1 * s));

      end;

      then ||.PL.|| <= ||.PQL.|| by LMINEQ;

      hence thesis by A4, A5, A24, XXREAL_0: 1;

    end;

    

     LMCL1: for X be RealNormSpace, Y,Z be Subset of X st Z = the carrier of ( Lin Y) holds ( Cl Z) is non empty

    proof

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

      assume

       A1: Z = the carrier of ( Lin Y);

      Z c= ( Cl Z) by PRETOPC18;

      hence ( Cl Z) is non empty by A1;

    end;

    begin

    definition

      let X be RealNormSpace, Y be Subset of X;

      :: NORMSP_3:def20

      func ClNLin (Y) -> non empty NORMSTR means

      : defClN: ex Z be Subset of X st Z = the carrier of ( Lin Y) & it = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),X)), ( Add_ (( Cl Z),X)), ( Mult_ (( Cl Z),X)), ( Norm_ (( Cl Z),X)) #);

      correctness

      proof

        reconsider Z = the carrier of ( Lin Y) as Subset of X by RLSUB_1:def 2;

        reconsider T = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),X)), ( Add_ (( Cl Z),X)), ( Mult_ (( Cl Z),X)), ( Norm_ (( Cl Z),X)) #) as non empty NORMSTR by LMCL1;

        ex Z be Subset of X st Z = the carrier of ( Lin Y) & T = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),X)), ( Add_ (( Cl Z),X)), ( Mult_ (( Cl Z),X)), ( Norm_ (( Cl Z),X)) #);

        hence thesis;

      end;

    end

    theorem :: NORMSP_3:68

    

     RSSPACE11: for X be RealNormSpace, V1 be Subset of X, CL be Subset of X st CL = the carrier of ( ClNLin V1) holds RLSStruct (# CL, ( Zero_ (CL,X)), ( Add_ (CL,X)), ( Mult_ (CL,X)) #) is Subspace of X

    proof

      let X be RealNormSpace, V1 be Subset of X, CL be Subset of X;

      assume

       A1: CL = the carrier of ( ClNLin V1);

      consider Z be Subset of X such that

       A2: Z = the carrier of ( Lin V1) & ( ClNLin V1) = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),X)), ( Add_ (( Cl Z),X)), ( Mult_ (( Cl Z),X)), ( Norm_ (( Cl Z),X)) #) by defClN;

      thus thesis by A1, RSSPACE: 11, A2, Cl01;

    end;

    

     SUBTHCL: for V be RealNormSpace, V1 be Subset of V, x,y be Point of V, x1,y1 be Point of ( ClNLin V1), a be Real st x = x1 & y = y1 holds ||.x.|| = ||.x1.|| & (x + y) = (x1 + y1) & (a * x) = (a * x1)

    proof

      let V be RealNormSpace, V1 be Subset of V, x,y be Point of V, x1,y1 be Point of ( ClNLin V1), a be Real;

      assume

       A1: x = x1 & y = y1;

      set l = ( ClNLin V1);

      consider Z be Subset of V such that

       A2: Z = the carrier of ( Lin V1) & l = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),V)), ( Add_ (( Cl Z),V)), ( Mult_ (( Cl Z),V)), ( Norm_ (( Cl Z),V)) #) by defClN;

      reconsider W = the RLSStruct of l as Subspace of V by A2, RSSPACE11;

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

      

      thus ||.x1.|| = ((the normF of V | ( Cl Z)) . x1) by A2, DefNorm

      .= ||.x.|| by A1, A2, FUNCT_1: 49;

      

      thus (x + y) = (x2 + y2) by A1, RLSUB_1: 13

      .= (x1 + y1);

      

      thus (a * x) = (a * x2) by A1, RLSUB_1: 14

      .= (a * x1);

    end;

    theorem :: NORMSP_3:69

    

     CLTh37: for X be RealNormSpace, Y be Subset of X, f,g be Point of ( ClNLin Y), a be Real holds ( ||.f.|| = 0 iff f = ( 0. ( ClNLin Y))) & ||.(a * f).|| = ( |.a.| * ||.f.||) & ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

    proof

      let X be RealNormSpace, Y be Subset of X;

      let f,g be Point of ( ClNLin Y);

      let a be Real;

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

      reconsider CL = ( Cl Z) as Subset of X;

      reconsider f1 = f, g1 = g as Point of X by A1, TARSKI:def 3;

      

       A3: (f1 + g1) = (f + g) by SUBTHCL;

      

       A4: (a * f1) = (a * f) by SUBTHCL;

      

       A5: ||.(f + g).|| = ||.(f1 + g1).|| by A3, SUBTHCL;

      

       A6: ||.(a * f).|| = ||.(a * f1).|| by A4, SUBTHCL;

      

       A7: ||.f.|| = ||.f1.|| by SUBTHCL;

      

       A8: ||.g.|| = ||.g1.|| by SUBTHCL;

      ( 0. ( ClNLin Y)) = ( 0. X) by A1, Cl01, RSSPACE:def 10;

      hence thesis by A5, A6, A7, A8, NORMSP_0:def 5, NORMSP_1:def 1;

    end;

    registration

      let X be RealNormSpace, Y be Subset of X;

      cluster ( ClNLin Y) -> reflexive discerning RealNormSpace-like;

      correctness by CLTh37;

    end

    theorem :: NORMSP_3:70

    

     CLTh39: for V be RealNormSpace, V1 be Subset of V holds ( ClNLin V1) is RealNormSpace

    proof

      let V be RealNormSpace, V1 be Subset of V;

      set l = ( ClNLin V1);

      consider Z be Subset of V such that

       A1: Z = the carrier of ( Lin V1) & l = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),V)), ( Add_ (( Cl Z),V)), ( Mult_ (( Cl Z),V)), ( Norm_ (( Cl Z),V)) #) by defClN;

      reconsider W = the RLSStruct of l as Subspace of V by A1, RSSPACE11;

      W is RealLinearSpace;

      hence thesis by RSSPACE3: 2;

    end;

    registration

      let X be RealNormSpace, Y be Subset of X;

      cluster ( ClNLin Y) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence by CLTh39;

    end

    theorem :: NORMSP_3:71

    

     CLTh40: for V be RealNormSpace, V1 be Subset of V holds ( ClNLin V1) is SubRealNormSpace of V

    proof

      let V be RealNormSpace, V1 be Subset of V;

      set l = ( ClNLin V1);

      consider Z be Subset of V such that

       A1: Z = the carrier of ( Lin V1) & ( ClNLin V1) = NORMSTR (# ( Cl Z), ( Zero_ (( Cl Z),V)), ( Add_ (( Cl Z),V)), ( Mult_ (( Cl Z),V)), ( Norm_ (( Cl Z),V)) #) by defClN;

      reconsider CL = ( Cl Z) as Subset of V;

      

       A3: ( 0. ( ClNLin V1)) = ( 0. V) by A1, Cl01, RSSPACE:def 10;

      

       A4: the addF of l = (the addF of V || the carrier of l) by A1, Cl01, RSSPACE:def 8;

      

       A5: the Mult of l = (the Mult of V | [: REAL , the carrier of l:]) by A1, Cl01, RSSPACE:def 9;

      the normF of l = (the normF of V | the carrier of l) by A1, DefNorm;

      hence thesis by A1, A3, A4, A5, DUALSP01:def 16;

    end;

    definition

      let V be RealNormSpace, V1 be Subset of V;

      :: original: ClNLin

      redefine

      func ClNLin (V1) -> SubRealNormSpace of V ;

      coherence by CLTh40;

    end