environ
vocabularies HIDDEN, RLSUB_1, HAHNBAN, UNIALG_1, DUALSP01, PROB_2, NFCONT_1, CFCONT_1, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, REALSET1, SEQ_1, 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, VALUED_1, METRIC_1, RELAT_2, ASYMPT_1, FUNCT_7, PARTFUN1, RCOMP_1, BHSP_1, RSSPACE2, DUALSP04, RUSUB_5, SQUARE_1, RVSUM_1, BHSP_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, REALSET1, NUMBERS, XCMPLX_0, SQUARE_1, XXREAL_0, XREAL_0, COMPLEX1, XXREAL_2, VALUED_1, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, RLSUB_1, RUSUB_1, RUSUB_5, NORMSP_0, NORMSP_1, HAHNBAN, RSSPACE, RSSPACE2, BHSP_6, RSSPACE3, LOPBAN_1, NFCONT_1, DUALSP01;
definitions ALGSTR_0, HAHNBAN, XXREAL_2, TARSKI;
theorems SEQ_4, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, COMPLEX1, TARSKI, RSSPACE3, XREAL_0, XXREAL_0, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, XCMPLX_0, RLVECT_1, FUNCOP_1, HAHNBAN, RSSPACE, ORDINAL1, NAT_1, BHSP_1, BHSP_2, BHSP_3, SUBSET_1, NFCONT_1, XXREAL_2, DUALSP01, XCMPLX_1, RUSUB_5, SQUARE_1, RUSUB_1, BHSP_6;
schemes FUNCT_2, XBOOLE_0;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1, XXREAL_0, VALUED_0, RLVECT_1, FUNCT_2, VALUED_1, FUNCOP_1, RELSET_1, NORMSP_3, XCMPLX_0, NAT_1, NORMSP_1, SEQ_2, DUALSP01, XBOOLE_0, SQUARE_1, RUSUB_1;
constructors HIDDEN, REAL_1, REALSET1, RSSPACE3, LOPBAN_2, SEQ_1, NFCONT_1, DUALSP01, RELSET_1, SEQ_2, SEQ_4, HAHNBAN1, COMSEQ_2, BHSP_2, BHSP_3, RUSUB_5, SQUARE_1, BHSP_6;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0, SEQ_1, BHSP_1, DUALSP01;
expansions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, FUNCT_2, SEQ_2, NORMSP_0, ORDINAL1, NORMSP_1, STRUCT_0, RLVECT_1, XXREAL_2, BHSP_1, MEMBERED, NFCONT_1, DUALSP01;
Lm01:
for X being RealUnitarySpace holds NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X,(normRU X) #) is RealNormSpace
Th16:
for X being RealUnitarySpace
for f being linear-Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds
f is Lipschitzian
Th17:
for X being RealUnitarySpace holds BoundedLinearFunctionals X is linearly-closed
Th27X:
for X being RealUnitarySpace
for g being Lipschitzian linear-Functional of X holds PreNorms g is bounded_above
Th23:
for X being RealUnitarySpace
for f being Lipschitzian linear-Functional of X holds Bound2Lipschitz (f,X) = f
Lm88A:
for X being RealUnitarySpace
for x, y being Point of X holds (||.(x + y).|| * ||.(x + y).||) + (||.(x - y).|| * ||.(x - y).||) = (2 * (||.x.|| * ||.x.||)) + (2 * (||.y.|| * ||.y.||))
KERX1:
for X being RealUnitarySpace
for f being Function of X,REAL st f is homogeneous holds
not f " {0} is empty