environ
vocabularies HIDDEN, GROUP_1, COMPLFLD, SUPINF_2, CARD_1, MATRIX_1, NUMBERS, ARYTM_3, ARYTM_1, RELAT_1, XCMPLX_0, SUBSET_1, FINSEQ_1, TREES_1, VECTSP_1, NAT_1, ALGSTR_0, FUNCT_1, BINOP_2, COMPLEX1, XXREAL_0, VALUED_0, TARSKI, ORDINAL4, MATRIX_5;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NAT_D, RELAT_1, FUNCT_1, VALUED_0, MATRIX_0, STRUCT_0, ALGSTR_0, FINSEQ_1, BINOP_1, MATRIX_3, MATRIX_1, NUMBERS, MATRIX_4, COMPLEX1, COMPLFLD, XCMPLX_0, GROUP_1, BINOP_2, XXREAL_0, VECTSP_1, RLVECT_1;
definitions ;
theorems FINSEQ_1, FUNCT_1, NAT_1, RLVECT_1, MATRIX_3, VECTSP_1, MATRIX_4, COMPLFLD, COMPLEX1, GROUP_1, BINOP_2, FINSEQ_3, XCMPLX_0, XREAL_1, VALUED_0, XXREAL_0, XREAL_0, MATRIX_0, RVSUM_1;
schemes NAT_1;
registrations RELSET_1, XCMPLX_0, XREAL_0, STRUCT_0, VECTSP_1, COMPLFLD, ORDINAL1, RVSUM_1, FINSEQ_1, NAT_1, MEMBERED;
constructors HIDDEN, BINOP_1, COMPLFLD, FVSUM_1, MATRIX_3, MATRIX_4, BINOP_2, NAT_D, RVSUM_1, RELSET_1, MATRIX_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities MATRIX_4, ORDINAL1;
expansions ;