environ
vocabularies HIDDEN, NUMBERS, NAT_1, SUBSET_1, FINSEQ_2, PRE_TOPC, EUCLID, RVSUM_1, FUNCT_1, CARD_1, FINSEQ_1, RELAT_1, VALUED_0, ARYTM_3, COMPLEX1, SQUARE_1, ARYTM_1, CARD_3, XXREAL_0, TARSKI, FUNCT_3, SUPINF_2, REAL_1;
notations HIDDEN, TARSKI, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, FINSEQ_1, FINSEQ_2, VALUED_0, QUIN_1, STRUCT_0, PRE_TOPC, RVSUM_1, RLVECT_1, EUCLID, SQUARE_1, XXREAL_0;
definitions ;
theorems EUCLID, RVSUM_1, FINSEQ_2, FINSEQ_1, FINSEQ_3, SQUARE_1, QUIN_1, ABSVALUE, TOPRNS_1, COMPLEX1, XREAL_1, XXREAL_0, FUNCOP_1, XCMPLX_1, FINSEQOP, ORDINAL1, FUNCT_1, CARD_1;
schemes ;
registrations FUNCT_1, RELSET_1, NUMBERS, XREAL_0, SQUARE_1, BINOP_2, MEMBERED, FINSEQ_2, MONOID_0, EUCLID, VALUED_0, FINSEQ_1, QUIN_1;
constructors HIDDEN, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, QUIN_1, FINSEQOP, MONOID_0, TOPRNS_1, RELSET_1, BINOP_1;
requirements HIDDEN, REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities SQUARE_1, FINSEQ_2, RVSUM_1, VALUED_1, ALGSTR_0, ORDINAL1;
expansions RVSUM_1;