environ
vocabularies HIDDEN, PRE_TOPC, RLVECT_1, FUNCT_1, ARYTM_3, ARYTM_1, FINSEQ_1, VALUED_1, MSSUBFAM, FINSEQ_2, CARD_3, RVSUM_1, RELAT_1, COMPLEX1, SQUARE_1, RCOMP_1, PARTFUN1, NORMSP_1, XBOOLE_0, LOPBAN_1, FDIFF_1, REAL_NS1, BORSUK_1, EUCLID, NUMBERS, FUNCOP_1, STRUCT_0, UNIALG_1, EUCLID_7, MATRIXR2, RFINSEQ2, REAL_1, SUBSET_1, CARD_1, TARSKI, XXREAL_0, NAT_1, ORDINAL4, SUPINF_2, VALUED_2, FCONT_1, XCMPLX_0;
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, FUNCOP_1, STRUCT_0, RLVECT_1, FINSEQ_1, FINSEQ_2, SQUARE_1, VALUED_1, VALUED_2, RVSUM_1, VECTSP_1, PRE_TOPC, VFUNCT_1, NORMSP_0, EUCLID, LOPBAN_1, NFCONT_1, NDIFF_1, REAL_NS1, PDIFF_1, INTEGR15, EUCLID_7, RFINSEQ2;
definitions LOPBAN_1;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, EUCLID, XREAL_1, XCMPLX_0, RLVECT_1, COMPLEX1, FINSEQ_1, FINSEQ_2, ORDINAL1, NAT_1, XXREAL_0, RVSUM_1, RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, SQUARE_1, INTEGR15, FUNCOP_1, EUCLID_7, FINSEQ_4, FINSEQ_5, NORMSP_1, LOPBAN_1, PARTFUN1, PARTFUN2, NFCONT_1, NDIFF_1, REAL_NS1, VALUED_1, PDIFF_1, RFINSEQ2, RLVECT_4, JORDAN2C, VECTSP_1, NORMSP_0, VALUED_2, XREAL_0;
schemes FUNCT_2, NAT_1, FINSEQ_1, RECDEF_1;
registrations RELSET_1, STRUCT_0, XREAL_0, LOPBAN_1, FUNCT_2, NAT_1, REAL_NS1, NUMBERS, XBOOLE_0, XXREAL_0, VALUED_0, EUCLID, CARD_1, VALUED_2, SQUARE_1, FINSEQ_1, RVSUM_1, ORDINAL1;
constructors HIDDEN, REAL_1, SQUARE_1, RSSPACE3, FINSEQOP, VFUNCT_1, COMPLEX1, NFCONT_1, NDIFF_1, PDIFF_1, BINOP_2, MONOID_0, INTEGR15, RELSET_1, EUCLID_7, RFINSEQ2, JORDAN2B, VALUED_2, XREAL_0;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities LOPBAN_1, RVSUM_1, EUCLID, VALUED_1, FINSEQ_1, XCMPLX_0, RFINSEQ2, SQUARE_1;
expansions LOPBAN_1;
:: Normed Linear Spaces $ {\cal R}^n$