environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, XBOOLE_0, ALGSTR_0, WELLORD1, QUOFIELD, RELAT_1, FUNCT_1, SUBSET_1, STRUCT_0, ORDINAL2, TARSKI, ORDINAL3, PRE_POLY, ARYTM_3, CARD_1, PBOOLE, FINSET_1, VALUED_0, FUNCOP_1, RLVECT_1, LATTICES, BINOP_1, POLYNOM1, FINSEQ_1, CARD_3, PARTFUN1, FINSEQ_2, NAT_1, VECTSP_1, ZFMISC_1, GROUP_1, SUPINF_2, XXREAL_0, FINSEQ_3, ORDINAL4, ARYTM_1, ORDERS_1, MSSUBFAM, POLYNOM6;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, VALUED_0, VECTSP_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, POLYNOM1, STRUCT_0, ALGSTR_0, NAT_1, NAT_D, ORDERS_1, PBOOLE, RLVECT_1, FINSET_1, FINSEQ_1, FINSEQ_2, ORDINAL2, ORDINAL3, GROUP_1, QUOFIELD, GRCAT_1, WSIERP_1, PRE_POLY, FVSUM_1, POLYNOM3, GROUP_6, XXREAL_0, MATRLIN;
definitions VECTSP_1, QUOFIELD, FUNCT_1, TARSKI, XBOOLE_0, FUNCT_2, STRUCT_0, VALUED_0, RINGCAT1, MOD_4;
theorems POLYNOM1, TOPGRP_1, FUNCT_2, PBOOLE, FUNCT_1, ORDINAL3, ORDINAL1, ORDINAL2, FINSEQ_3, FINSEQ_2, FVSUM_1, FINSEQ_1, RELAT_1, FUNCOP_1, POLYALG1, FINSEQ_5, VECTSP_1, FINSEQ_4, FINSET_1, TARSKI, POLYNOM2, MATRLIN, RLVECT_1, NAT_1, SUBSET_1, CARD_3, POLYNOM3, ORDERS_1, RVSUM_1, XBOOLE_0, XBOOLE_1, XREAL_1, GROUP_6, XXREAL_0, GROUP_1, PARTFUN1, NAT_D, PRE_POLY;
schemes PBOOLE, FUNCT_2, FRAENKEL, FUNCT_1, RECDEF_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, QUOFIELD, PRE_POLY, POLYNOM1, POLYNOM2, VALUED_0, CARD_1;
constructors HIDDEN, ORDINAL3, BINARITH, WSIERP_1, GRCAT_1, GROUP_6, TRIANG_1, QUOFIELD, POLYNOM1, POLYNOM3, NAT_D, RELSET_1, MATRLIN, FVSUM_1, RINGCAT1, MOD_4;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL;
equalities XBOOLE_0, STRUCT_0, ORDINAL1;
expansions FUNCT_1, XBOOLE_0;