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, GROUP_7, FUNCOP_1, ALGSTR_0, GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1, ORDINAL4, ARYTM_1, ARYTM_3, FINSET_1, ZFMISC_1, PBOOLE, REALSET1, NEWTON, GROUP_4, FINSEQ_2, PRE_POLY, UPROOTS, GROUP_19, SEMI_AF1, MONOID_0, QC_LANG1, RLSUB_1, VECTMETR;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, FUNCOP_1, REALSET1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, FINSEQ_1, FINSEQ_2, FUNCT_7, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_4, GROUP_6, MONOID_0, PRALG_1, GRSOLV_1, GROUP_7, GROUP_12, GROUP_17;
definitions ;
theorems PRALG_1, FUNCT_1, CARD_3, FUNCT_2, FUNCOP_1, TARSKI, GROUP_1, GROUP_2, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_6, FINSEQ_2, XREAL_1, FINSEQ_3, XBOOLE_0, RELAT_1, GROUP_7, FUNCT_7, CARD_2, XBOOLE_1, REALSET1, GROUP_12, PARTFUN1, ZFMISC_1, GROUP_17;
schemes NAT_1, FUNCT_2, XBOOLE_0, CLASSES1;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1, FUNCT_2, CARD_3, GROUP_7, RELSET_1, SUBSET_1, INT_1, GR_CY_1, FINSET_1, RELAT_1, FUNCT_1, NUMBERS, GROUP_12, PBOOLE;
constructors HIDDEN, REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_12, GROUP_4, FUNCT_7, RELSET_1, FUNCT_3, GROUP_17, GRSOLV_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GROUP_2, FINSEQ_1, STRUCT_0, GRSOLV_1;
expansions STRUCT_0, TARSKI, FINSEQ_1, MONOID_0;