environ
vocabularies HIDDEN, FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1, GROUP_1, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, FUNCOP_1, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, FINSET_1, NEWTON, GROUP_4, PRE_POLY, UPROOTS, GROUP_19, SEMI_AF1, QC_LANG1, VECTMETR, GROUP_20;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, FINSEQ_1, FUNCT_7, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, PRALG_1, GRSOLV_1, GROUP_7, GROUP_12, GROUP_19;
definitions ;
theorems FUNCT_1, CARD_3, FUNCT_2, FUNCOP_1, TARSKI, GROUP_1, GROUP_2, GROUP_3, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_6, FINSEQ_2, XREAL_1, FINSEQ_3, XBOOLE_0, RELAT_1, GROUP_7, FUNCT_7, XBOOLE_1, GROUP_12, PARTFUN1, ZFMISC_1, GROUP_17, GROUP_19, GRSOLV_1;
schemes NAT_1, FUNCT_1, CLASSES1;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1, FUNCT_2, FUNCOP_1, CARD_1, GROUP_7, GROUP_3, RELSET_1, SUBSET_1, INT_1, FINSET_1, RELAT_1, FUNCT_1, NUMBERS, GROUP_12, GROUP_6, GROUP_19;
constructors HIDDEN, REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_4, FUNCT_7, RELSET_1, INT_7, FUNCT_3, GROUP_17, GRSOLV_1, GROUP_19;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GROUP_2, FINSEQ_1, STRUCT_0, FUNCOP_1, GRSOLV_1, GROUP_19, SUBSET_1;
expansions STRUCT_0, TARSKI;