environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, VALUED_0, FUNCT_1, XCMPLX_0, ARYTM_1, RELAT_1, ARYTM_3, CARD_1, MEMBERED, PARTFUN1, TARSKI, ORDINAL4, VALUED_1, COMPLEX1, FUNCT_3, XXREAL_2, XXREAL_0, REAL_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_3, VALUED_0, VALUED_1, COMSEQ_2, SEQ_2, REAL_1;
definitions TARSKI, PARTFUN1, XBOOLE_0, VALUED_0, SEQ_2;
theorems TARSKI, FUNCT_1, FUNCT_3, ABSVALUE, PARTFUN1, PARTFUN2, RELSET_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, VALUED_0, VALUED_1, SEQ_2, XREAL_0;
schemes FUNCT_1;
registrations FUNCT_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, VALUED_1, XCMPLX_0, SEQ_2, XXREAL_0, RELAT_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, FUNCT_3, XXREAL_0, REAL_1, COMPLEX1, VALUED_1, PARTFUN2, SEQ_2, RELSET_1, COMSEQ_2;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities XBOOLE_0, VALUED_1, ORDINAL1;
expansions TARSKI, PARTFUN1, XBOOLE_0, SEQ_2;
Lm1:
(- 1) " = - 1
;
::OPERATIONS ON PARTIAL FUNCTIONS FROM A DOMAIN, TO THE SET OF REAL NUMBERS
::