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