environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, XCMPLX_0, COMSEQ_1, PARTFUN1, ORDINAL2, NAT_1, FDIFF_1, VALUED_0, SEQ_2, CARD_1, SEQ_1, FUNCT_1, COMPLEX1, RELAT_1, ARYTM_3, XXREAL_0, ARYTM_1, FUNCOP_1, VALUED_1, FUNCT_2, TARSKI, RCOMP_1, XBOOLE_0, FCONT_1, CFCONT_1, XXREAL_2, CFDIFF_1, FUNCT_7, ASYMPT_1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, FUNCT_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, PARTFUN1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, RELSET_1, SEQ_2, CFUNCT_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, CFCONT_1, XXREAL_0;
definitions XBOOLE_0, TARSKI, COMSEQ_2, CFCONT_1, FUNCT_2;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, COMPLEX1, SEQ_1, SEQ_2, SEQ_4, COMSEQ_1, COMSEQ_2, CFUNCT_1, CFCONT_1, RELAT_1, XBOOLE_0, XBOOLE_1, PARTFUN1, PARTFUN2, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, ORDINAL1, ABSVALUE, XREAL_0, FUNCOP_1, SUBSET_1, VALUED_1, VALUED_0;
schemes SEQ_1, COMSEQ_1, FUNCT_2;
registrations FUNCT_1, RELSET_1, FUNCT_2, MEMBERED, NUMBERS, ORDINAL1, XREAL_0, XXREAL_0, COMSEQ_2, NAT_1, VALUED_0, VALUED_1, FUNCOP_1, XCMPLX_0, SEQ_2, CFUNCT_1, SEQ_1;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, VALUED_0, VALUED_1, SEQ_2, FINSEQ_4, SEQM_3, PARTFUN2, SQUARE_1, COMSEQ_2, COMSEQ_3, CFCONT_1, XXREAL_0, CFUNCT_1, RELSET_1, SEQ_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XCMPLX_0, XBOOLE_0, SUBSET_1, VALUED_1, COMPLEX1;
expansions XBOOLE_0, TARSKI, COMSEQ_2, FUNCT_2;
reconsider cs = NAT --> 0c as Complex_Sequence ;
reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX ;
Lm1:
for z0 being Complex
for N1, N2 being Neighbourhood of z0 ex N being Neighbourhood of z0 st
( N c= N1 & N c= N2 )