environ
vocabularies HIDDEN, PETRI_DF, NUMBERS, XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, TARSKI, PETRI, FUNCT_2, ARYTM_3, FINSEQ_1, PARTFUN1, XXREAL_0, CARD_1, CARD_3, ORDINAL4, NAT_1, ARYTM_1, BOOLMARK, STRUCT_0, PNPROC_1, ZFMISC_1, INT_1, FINSET_1, AOFA_I00, NET_1, FINSEQ_4, RFINSEQ, FINSEQ_6, JORDAN23;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, PARTFUN1, FUNCT_2, DOMAIN_1, XXREAL_0, STRUCT_0, ZFMISC_1, RELSET_1, FINSEQ_1, PARTIT_2, PETRI, FINSET_1, NAT_D, WSIERP_1, RLAFFIN3, NET_1, FINSEQ_6, FINSEQ_4, JORDAN23, RFINSEQ;
definitions XBOOLE_0, TARSKI, JORDAN23;
theorems TARSKI, ZFMISC_1, PETRI, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_4, NAT_1, FINSEQ_2, FINSEQ_3, RELAT_1, XBOOLE_0, XREAL_1, XXREAL_0, PARTFUN1, SEQ_4, NAT_D, RLAFFIN3, BOOLMARK, NET_1, RVSUM_1, FINSEQ_5, RFINSEQ, JORDAN23;
schemes NAT_1, DOMAIN_1, FUNCT_2, FINSEQ_1, FRAENKEL;
registrations XXREAL_0, XREAL_0, FINSEQ_1, ORDINAL1, CARD_1, RELSET_1, STRUCT_0, XBOOLE_0, SUBSET_1, XTUPLE_0, FINSET_1, NAT_1, MEMBERED, VALUED_0, PETRI;
constructors HIDDEN, PARTIT_2, NAT_D, WSIERP_1, RLAFFIN3, NET_1, FINSEQ_4, FINSEQ_6, RFINSEQ, JORDAN23;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities PETRI, NET_1;
expansions FINSEQ_6;