environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0, CARD_1, XBOOLE_0, ORDINAL4, CARD_3, FINSOP_1, BINOP_2, INT_1, SERIES_1, VALUED_1, PREPOWER, NEWTON, POWER, NUMERAL1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, CARD_1, XCMPLX_0, XXREAL_0, AFINSQ_1, VALUED_1, RELSET_1, FUNCT_2, BINOP_1, NAT_1, BINOP_2, RECDEF_1, SERIES_1, NEWTON, PREPOWER, POWER, AFINSQ_2, NAT_D;
definitions TARSKI;
theorems TARSKI, FUNCT_1, NAT_1, RELAT_1, ORDINAL1, CARD_1, XREAL_1, XXREAL_0, AFINSQ_2, AFINSQ_1, FUNCT_2, NAT_2, INT_1, NEWTON, BINOP_2, SERIES_1, SEQ_1, PREPOWER, POWER, XCMPLX_1, PEPIN, PRE_FF, NAT_D;
schemes NAT_1, AFINSQ_2, AFINSQ_1, STIRL2_1;
registrations XBOOLE_0, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, CARD_1, NUMBERS, INT_1, BINOP_2, MEMBERED, NEWTON, AFINSQ_1, VALUED_1, FUNCT_2, POWER, FINSET_1, AFINSQ_2, RELSET_1, VALUED_0, FUNCT_1;
constructors HIDDEN, PREPOWER, SERIES_1, PARTFUN3, BINOM, SETWISEO, REAL_1, NAT_D, RECDEF_1, BINOP_2, RELSET_1, AFINSQ_2, BINOP_1, NEWTON;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ORDINAL1, CARD_1;
expansions ;