environ
vocabularies HIDDEN, XBOOLE_0, CLVECT_1, PARTFUN1, XCMPLX_0, SUBSET_1, ARYTM_3, ARYTM_1, RELAT_1, NUMBERS, VALUED_1, NORMSP_1, FUNCT_1, SUPINF_2, CARD_1, TARSKI, COMPLEX1, VFUNCT_1, REAL_1, XXREAL_0, XXREAL_2, RLVECT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, STRUCT_0, RLVECT_1, VALUED_1, COMSEQ_2, COMPLEX1, NORMSP_0, CLVECT_1, XXREAL_0, VFUNCT_1;
definitions TARSKI, PARTFUN1, XBOOLE_0;
theorems TARSKI, SUBSET_1, FUNCT_1, ABSVALUE, PARTFUN1, PARTFUN2, RFUNCT_1, RLVECT_1, RELAT_1, XREAL_0, XBOOLE_0, XBOOLE_1, CLVECT_1, COMPLEX1, CFUNCT_1, XREAL_1, XXREAL_0, VALUED_1, NORMSP_0, VFUNCT_1;
schemes PARTFUN2;
registrations RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, VALUED_0, RFUNCT_1, XCMPLX_0;
constructors HIDDEN, REAL_1, COMPLEX1, CLVECT_1, VALUED_1, RELSET_1, VFUNCT_1, COMSEQ_2;
requirements HIDDEN, SUBSET, BOOLE, ARITHM, NUMERALS;
equalities XBOOLE_0, RLVECT_1, VALUED_1;
expansions PARTFUN1, XBOOLE_0;
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN TO THE SET OF COMPLEX NUMBERS
::