environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, NORMSP_1, NAT_1, SUBSET_1, FUNCT_1, SUPINF_2, SERIES_1, ARYTM_3, CARD_1, SEQ_2, FUNCOP_1, REAL_1, XXREAL_0, ARYTM_1, CARD_3, ORDINAL2, RSSPACE3, VALUED_0, RELAT_1, COMPLEX1, XXREAL_2, LOPBAN_1, SEQ_1, POWER, LOPBAN_2, MESFUNC1, REWRITE1, VECTSP_1, BINOP_1, PREPOWER, STRUCT_0, COMSEQ_3, PRE_TOPC, VALUED_1, LOPBAN_3;
notations HIDDEN, TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, DOMAIN_1, FUNCOP_1, XREAL_0, XXREAL_0, XCMPLX_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, NUMBERS, RLVECT_1, GROUP_1, VECTSP_1, NORMSP_0, NORMSP_1, RSSPACE3, VALUED_1, SEQ_1, SEQ_2, VALUED_0, SERIES_1, PREPOWER, POWER, BHSP_4, LOPBAN_1, LOPBAN_2, RECDEF_1;
definitions SEQ_2, SERIES_1, NORMSP_1, ALGSTR_0, VECTSP_1;
theorems ABSVALUE, RLVECT_1, VECTSP_1, FUNCSDOM, SEQ_1, SEQ_2, SEQM_3, SERIES_1, NAT_1, INT_1, FUNCT_2, NORMSP_1, SEQ_4, RSSPACE3, LOPBAN_1, PREPOWER, LOPBAN_2, GROUP_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, BHSP_4, VALUED_0, ALGSTR_0, NORMSP_0;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, NORMSP_1, LOPBAN_2, ALGSTR_0, GCD_1, VALUED_1, FUNCT_2, VALUED_0, FUNCOP_1, NORMSP_0, NAT_1, INT_1;
constructors HIDDEN, DOMAIN_1, REAL_1, COMPLEX1, SEQ_2, BINOP_2, PREPOWER, SERIES_1, BHSP_4, RSSPACE3, LOPBAN_2, GCD_1, RECDEF_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities BINOP_1, ALGSTR_0;
expansions SERIES_1, NORMSP_1, ALGSTR_0;
Lm1:
for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
Lm2:
for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
Lm3:
for X being RealNormSpace
for x, y being Point of X
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Nat holds ||.(x - y).|| <= seq . n ) holds
x = y