environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, CLVECT_1, NAT_1, SUBSET_1, FUNCT_1, SUPINF_2, SERIES_1, ARYTM_3, CARD_1, SEQ_2, FUNCOP_1, REAL_1, XXREAL_0, NORMSP_1, ARYTM_1, CARD_3, ORDINAL2, LOPBAN_3, RSSPACE3, VALUED_0, RELAT_1, COMPLEX1, XCMPLX_0, XXREAL_2, CLOPBAN1, SEQ_1, POWER, CLOPBAN2, MESFUNC1, VECTSP_1, PREPOWER, STRUCT_0, COMSEQ_3, PRE_TOPC, VALUED_1;
notations HIDDEN, TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, DOMAIN_1, FUNCOP_1, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, NUMBERS, RLVECT_1, VECTSP_1, NORMSP_1, VALUED_1, SEQ_1, VALUED_0, SEQ_2, SERIES_1, PREPOWER, POWER, NORMSP_0, CLVECT_1, CSSPACE3, BHSP_4, CLOPBAN1, CLOPBAN2, LOPBAN_3, RECDEF_1;
definitions SEQ_2, SERIES_1, CLVECT_1, VECTSP_1;
theorems ABSVALUE, RLVECT_1, VECTSP_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, NAT_1, INT_1, FUNCT_2, SEQ_4, PREPOWER, CLVECT_1, CSSPACE3, LOPBAN_3, CLOPBAN1, CFUNCDOM, CLOPBAN2, GROUP_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, BHSP_4, NORMSP_1, VALUED_0, NORMSP_0;
schemes NAT_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, CLOPBAN2, VALUED_1, FUNCT_2, VALUED_0, FUNCOP_1, NORMSP_0, XCMPLX_0, NAT_1, INT_1, ALGSTR_0;
constructors HIDDEN, DOMAIN_1, REAL_1, COMPLEX1, SEQ_2, PREPOWER, SERIES_1, BHSP_4, CSSPACE3, CLOPBAN2, RECDEF_1, RELSET_1, BINOP_2, COMSEQ_2, BINOP_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities BINOP_1, ALGSTR_0;
expansions SERIES_1, CLVECT_1;
Lm1:
for X being ComplexNormSpace
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 ComplexNormSpace
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 ComplexNormSpace
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