:: Topological Properties of Real Normed Space
::  by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
:: 
:: Received September 15, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RLSUB_1, UNIALG_1, DUALSP01, NORMSP_3, CFCONT_1, MOD_4, RLVECT_1,
      ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, VECTSP_1, REAL_1, TARSKI,
      MSSUBFAM, STRUCT_0, REALSET1, FUNCOP_1, FCONT_1, NORMSP_0, SEQ_2,
      LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, PRE_TOPC,
      SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2,
      COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, METRIC_1, RELAT_2,
      PARTFUN1, RCOMP_1, TOPS_1, SETFAM_1, TOPGEN_1, CARD_3, NORMSP_2,
      RLVECT_3, VECTSP10, GROUP_6;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1,
      SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, REALSET1,
      NUMBERS, CARD_3, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, COMPLEX1,
      XXREAL_2, SEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, TOPS_1, RLVECT_1,
      RLVECT_3, RLSUB_1, VECTSP_1, VECTSP_4, NORMSP_0, NORMSP_1, NORMSP_2,
      HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, NFCONT_1, VECTSP10, DUALSP01,
      TOPGEN_1;
 constructors REALSET1, RSSPACE3, BINOP_2, LOPBAN_2, NFCONT_1, DUALSP01,
      RELSET_1, SEQ_4, NORMSP_2, CARD_3, PCOMPS_1, RLVECT_3, SETFAM_1, TOPS_1,
      VECTSP10, TOPGEN_1;
 registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1,
      XXREAL_0, VECTSP_1, FUNCT_2, SEQ_4, RELSET_1, TOPS_1, XCMPLX_0, NORMSP_0,
      NAT_1, NORMSP_1, XBOOLE_0, SUBSET_1, NORMSP_2, RLSUB_1, REALSET1,
      LOPBAN_1;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin :: Open and Closed Subsets

registration
  let X be RealNormSpace;
  cluster open closed for Subset of X;
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;
end;

theorem :: NORMSP_3:2
  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;
end;

registration
  let X be RealNormSpace;
  cluster [#]X -> closed;
  cluster {} X -> closed;
  cluster [#]X -> open;
  cluster {} X -> open;
end;

registration
  let X be RealNormSpace;
  let P,Q be closed Subset of X;
  cluster P /\ Q -> closed for Subset of X;
  cluster P \/ Q -> closed for Subset of X;
end;

registration
  let X be RealNormSpace;
  let P,Q be open Subset of X;
  cluster P /\ Q -> open for Subset of X;
  cluster P \/ Q -> open for Subset of X;
end;

definition
  let X be RealNormSpace, Y be Subset of X;
  func Cl Y -> Subset of X means
:: NORMSP_3:def 1

  ex Z be Subset of LinearTopSpaceNorm X st Z = Y & it = Cl Z;
end;

registration
  let X be RealNormSpace, Y be Subset of X;
  cluster Cl Y -> closed;
end;

theorem :: NORMSP_3:3
  for X be RealNormSpace,
      Y be Subset of X,
      Z be Subset of LinearTopSpaceNorm X
  st Y = Z
  holds Cl Y = Cl Z;

theorem :: NORMSP_3:4
  for X be RealNormSpace, Z be Subset of X holds Z c= Cl(Z);

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 being Subset of X
    st G is open & v in G
    holds G meets Y;

theorem :: NORMSP_3:6
  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;

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

theorem :: NORMSP_3:8
  for X be RealNormSpace, A,B being Subset of X
  st A c= B holds Cl A c= Cl B;

theorem :: NORMSP_3:9
  for X be RealNormSpace, A,B being Subset of X
  holds Cl(A \/ B) = Cl A \/ Cl B;

theorem :: NORMSP_3:10
  for X be RealNormSpace, A,B being Subset of X
  holds Cl (A /\ B) c= (Cl A) /\ Cl B;

theorem :: NORMSP_3:11
  for X be RealNormSpace, A being Subset of X
  holds A is closed iff Cl A = A;

theorem :: NORMSP_3:12
  for X be RealNormSpace, A being Subset of X
  holds A is open iff Cl([#](X) \ A) = [#](X) \ A;

theorem :: NORMSP_3:13
  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;

begin :: Density

definition
  let X be RealNormSpace, A be Subset of X;
  attr A is dense means
:: NORMSP_3:def 2
  Cl A = [#] X;
end;

registration
  let X be RealNormSpace;
  cluster [#]X -> dense;
end;

registration
  let X be RealNormSpace;
  cluster open closed dense for Subset of X;
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 ex seq be sequence of X
    st rng seq c= A & seq is convergent & lim seq = x;

theorem :: NORMSP_3:15
  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;

theorem :: NORMSP_3:16
  for X be RealNormSpace, R,S being Subset of X
  st R is dense & R c= S
  holds S is dense;

theorem :: NORMSP_3:17
  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;

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

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;

theorem :: NORMSP_3:20
  for X be RealNormSpace, A be Subset of X
  st A is dense holds A is non empty;

begin :: Separability

definition
  let X be RealNormSpace;
  attr X is separable means
:: NORMSP_3:def 3
  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;

begin :: Sequence and Convergence

theorem :: NORMSP_3:22
  for x,y,z be Real st 0 <= y
   & for e be Real st 0 < e holds x <= z + y*e
  holds x <= z;

theorem :: NORMSP_3:23
  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;

theorem :: NORMSP_3:24
  for X be RealNormSpace, x be Point of X holds {x} is closed;

theorem :: NORMSP_3:25
  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;

begin :: Subspace

theorem :: NORMSP_3:26
  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;

theorem :: NORMSP_3:27
  for V be RealNormSpace,
      W be SubRealNormSpace of V
  holds W is Subspace of V;

theorem :: NORMSP_3:28
  for V be RealNormSpace,
      V1 be SubRealNormSpace of V,
      x,y being Point of V,
      x1,y1 being Point of V1,
      a be Real
  st x = x1 & y = y1 holds
    ||.x.|| = ||.x1.||
  & x+y = x1+y1
  & a*x = a*x1;

theorem :: NORMSP_3:29
  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;

definition
  let X be RealNormSpace;
  let X1 be set;
  assume
   X1 c= the carrier of X;
  func Norm_(X1,X) -> Function of X1,REAL equals
:: NORMSP_3:def 4

  (the normF of X) | X1;
end;

definition
  let V be RealNormSpace, V1 be Subset of V;
  func NLin(V1) -> non empty NORMSTR equals
:: NORMSP_3:def 5
  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) #);
end;

theorem :: NORMSP_3:30
  for V be RealNormSpace, V1 be Subset of V
  holds NLin(V1) is SubRealNormSpace of V;

definition
  let V be RealNormSpace, V1 be Subset of V;
  redefine func NLin(V1) -> SubRealNormSpace of V;
end;

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

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;

begin :: Linear Functions

theorem :: NORMSP_3:33
  for X,Y be RealLinearSpace,
      f be Function of X, Y
  st f is homogeneous
  holds f"{0.Y} is non empty;

registration
  let X,Y be RealLinearSpace,
  f be LinearOperator of X,Y;
  cluster f"{0.Y} -> non empty;
end;

theorem :: NORMSP_3:34
  for X,Y be RealLinearSpace,
      f be Function of X, Y
  st f is additive homogeneous
  holds f"{0.Y} is linearly-closed;

theorem :: NORMSP_3:35
  for X,Y be RealLinearSpace,
      f be Function of X, Y
  st f is additive homogeneous
  holds rng f is linearly-closed;

definition
  let X,Y be RealLinearSpace,
      f be LinearOperator of X,Y;
  func Ker(f) -> Subspace of X equals
:: NORMSP_3:def 6
  Lin(f"{0.Y});
end;

definition
  let X,Y be RealNormSpace,
      f be LinearOperator of X,Y;
  func NKer(f) -> SubRealNormSpace of X equals
:: NORMSP_3:def 7
  NLin(f"{0.Y});
end;

definition
  let X,Y be RealLinearSpace,
      f be LinearOperator of X,Y;
  func Im(f) -> Subspace of Y equals
:: NORMSP_3:def 8
  Lin(rng f);
end;

definition
  let X,Y be RealNormSpace,
      f be LinearOperator of X,Y;
  func Im(f) -> SubRealNormSpace of Y equals
:: NORMSP_3:def 9
  NLin(rng f);
end;

definition
  let X,Y be RealLinearSpace,
      L be LinearOperator of X,Y;
  attr L is isomorphism means
:: NORMSP_3:def 10
  L is one-to-one onto;
end;

registration
  let X,Y be RealLinearSpace;
  cluster isomorphism -> one-to-one onto for LinearOperator of X,Y;
  cluster one-to-one onto -> isomorphism for LinearOperator of X,Y;
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;

definition
  let X,Y be RealNormSpace,
      L be LinearOperator of X,Y;
  attr L is isomorphism means
:: NORMSP_3:def 11
  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;
end;

theorem :: NORMSP_3:37
  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;

theorem :: NORMSP_3:38
  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);

theorem :: NORMSP_3:39
  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;

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;

theorem :: NORMSP_3:41
  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;

theorem :: NORMSP_3:42
  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;

theorem :: NORMSP_3:43
  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;

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;

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;

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;

begin :: Banach Space

theorem :: NORMSP_3:47
  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;

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;

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;

begin :: Quotient Vector Space

definition
  let X be RealLinearSpace,
      Y be Subspace of X;
  redefine func RLSp2RVSp Y -> Subspace of RLSp2RVSp X;
end;

definition
  let X be RealLinearSpace,
      Y be Subspace of X;
  func VectQuot(X,Y) -> RealLinearSpace equals
:: NORMSP_3:def 12
  RVSp2RLSp VectQuot(RLSp2RVSp X, RLSp2RVSp Y);
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
  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;

theorem :: NORMSP_3:53
  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;

definition
  let X be RealLinearSpace, Y be Subspace of X;
  func CosetSet(X,Y) -> non empty Subset-Family of X equals
:: NORMSP_3:def 13
  the set of all A where A is Coset of Y;
end;

definition
  let V be RealLinearSpace, W be Subspace of V;
  func zeroCoset(V,W) -> Element of CosetSet(V,W) equals
:: NORMSP_3:def 14
  the carrier of W;
end;

theorem :: NORMSP_3:54
  for X be RealLinearSpace, Y be Subspace of X
  holds CosetSet(X,Y) = CosetSet(RLSp2RVSp X,RLSp2RVSp Y);

theorem :: NORMSP_3:55
  for V be RealLinearSpace, W be Subspace of V
  holds the carrier of VectQuot(V,W) = CosetSet(V,W);

theorem :: NORMSP_3:56
  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;

theorem :: NORMSP_3:57
  for V be RealLinearSpace, W be Subspace of V
  holds 0. VectQuot(V,W) = zeroCoset(V,W);

theorem :: NORMSP_3:58
  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;

theorem :: NORMSP_3:59
  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;

theorem :: NORMSP_3:60
  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;

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;

theorem :: NORMSP_3:62
  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;

theorem :: NORMSP_3:63
  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;

definition
  let V be RealLinearSpace, W be Subspace of V;
  func InducedSur(V,W) -> LinearOperator of V, VectQuot(V,W) means
:: NORMSP_3:def 15

  it is onto & for v being VECTOR of V holds it.v = v + W;
end;

theorem :: NORMSP_3:64
  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;

definition
  let V,W be RealLinearSpace, L be LinearOperator of V,W;
  func InducedBi (V,W,L) -> LinearOperator of VectQuot(V,Ker L),Im L means
:: NORMSP_3:def 16

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

definition
  let V be RealNormSpace, W be Subspace of V, v be VECTOR of V;
  func NormVSets(V,W,v) -> non empty Subset of REAL equals
:: NORMSP_3:def 17
  {||.x.|| where x is VECTOR of V : x in v + W};
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;
end;

theorem :: NORMSP_3:66
  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.||;

definition
  let V be RealNormSpace, W be Subspace of V;
  func NormCoset(V,W) -> Function of CosetSet(V,W), REAL means
:: NORMSP_3:def 18

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

definition
  let X be RealNormSpace, Y be Subspace of X;
  assume
   ex CY be Subset of X st CY = the carrier of Y & CY is closed;
  func NVectQuot (X,Y) -> strict RealNormSpace means
:: NORMSP_3:def 19

  the RLSStruct of it = VectQuot (X,Y) & the normF of it = NormCoset(X,Y);
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;

begin :: Closure

definition
  let X be RealNormSpace, Y be Subset of X;
  func ClNLin(Y) -> non empty NORMSTR means
:: NORMSP_3:def 20

  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) #);
end;

theorem :: NORMSP_3:68
  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;

theorem :: NORMSP_3:69
  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.||;

registration
  let X be RealNormSpace, Y be Subset of X;
  cluster ClNLin(Y) -> reflexive discerning RealNormSpace-like;
end;

theorem :: NORMSP_3:70
  for V be RealNormSpace, V1 be Subset of V
  holds ClNLin(V1) is RealNormSpace;

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

theorem :: NORMSP_3:71
  for V be RealNormSpace, V1 be Subset of V
  holds ClNLin(V1) is SubRealNormSpace of V;

definition
  let V be RealNormSpace, V1 be Subset of V;
  redefine func ClNLin(V1) -> SubRealNormSpace of V;
end;