environ
vocabularies HIDDEN, NUMBERS, REAL_1, XCMPLX_0, NORMSP_1, CLVECT_1, PARTFUN1, NFCONT_2, TARSKI, RELAT_1, CARD_1, ARYTM_3, PRE_TOPC, ARYTM_1, STRUCT_0, COMPLEX1, XBOOLE_0, XXREAL_0, VALUED_1, SUPINF_2, FUNCT_1, CFCONT_1, NFCONT_1, SUBSET_1, RCOMP_1, NAT_1, VALUED_0, SEQ_2, ORDINAL2, FCONT_1, FUNCT_2, SEQ_4, CLOPBAN1, ALI2, FUNCOP_1, POWER, RSSPACE3, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PRE_TOPC, VALUED_0, STRUCT_0, RLVECT_1, FUNCOP_1, VALUED_1, SEQ_2, SEQ_4, FUNCT_7, VFUNCT_1, POWER, VFUNCT_2, NORMSP_0, NORMSP_1, CLVECT_1, NFCONT_1, CLOPBAN1, NFCONT_2, NCFCONT1, CSSPACE3;
definitions ;
theorems TARSKI, ABSVALUE, XBOOLE_1, RLVECT_1, XCMPLX_1, SEQ_2, NAT_1, RELAT_1, VFUNCT_1, FUNCT_2, SEQ_4, NORMSP_1, LOPBAN_3, PARTFUN2, CLVECT_1, CLOPBAN3, VFUNCT_2, NFCONT_1, CLOPBAN1, COMPLEX1, NCFCONT1, NFCONT_2, FUNCOP_1, POWER, CSSPACE3, FUNCT_7, SEQ_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, VALUED_0, NORMSP_0;
schemes FUNCT_2, NAT_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, VALUED_1, FUNCT_2, NUMBERS, VALUED_0, FUNCT_7, CLVECT_1, XCMPLX_0, NAT_1;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, SEQ_2, SEQ_4, POWER, FUNCT_7, CSSPACE3, NFCONT_1, NFCONT_2, CLOPBAN3, VFUNCT_2, NCFCONT1, RELSET_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1;
expansions ;
Lm1:
for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
Lm2:
for X being ComplexNormSpace
for x, y, z being Point of X
for e being Real st ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
Lm3:
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
Lm4:
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