environ
vocabularies HIDDEN, RELAT_1, XBOOLE_0, FUNCT_1, SUBSET_1, MSSUBFAM, FUNCT_2, CAYLEY, ALGSTR_0, GROUP_1, BINOP_1, STRUCT_0, WELLORD1, GROUP_6, NAT_1, FINSEQ_1, TARSKI, MONOID_0, FINSET_1, FUNCT_5, ZFMISC_1, MATRIX_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FINSET_1, FUNCT_2, BINOP_1, ORDINAL1, FINSEQ_1, FUNCT_5, PARTIT_2, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_6, MONOID_0, TOPGRP_1, MATRIX_1;
definitions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, STRUCT_0, MONOID_0, GROUP_1, GROUP_6;
theorems FUNCT_2, TOPGRP_1, FUNCT_1, GROUP_1, RELAT_1, BINOP_1, GROUP_6, MATRIX_1, WELLORD2, CARD_1, TARSKI, FUNCOP_1;
schemes FUNCT_2, BINOP_1;
registrations XBOOLE_0, FUNCT_1, PARTFUN1, GROUP_2, STRUCT_0, TOPGRP_1, FUNCT_2, MATRIX_1, RELSET_1, MONOID_0, FINSET_1, FRAENKEL, ZFMISC_1;
constructors HIDDEN, RELSET_1, GROUP_6, TOPGRP_1, BINOP_1, MATRIX_1, MONOID_0, WELLORD2, PARTIT_2, FUNCT_5;
requirements HIDDEN, SUBSET, BOOLE;
equalities FUNCT_5, ALGSTR_0, ORDINAL1;
expansions FUNCT_1, FUNCT_2, MONOID_0;