environ
vocabularies HIDDEN, GAUSSINT, NUMBERS, SUBSET_1, RLVECT_1, STRUCT_0, FUNCT_1, RAT_1, XBOOLE_0, ALGSTR_0, RELAT_1, ARYTM_3, CARD_3, BINOP_2, RLSUB_2, EQREL_1, PRELAMB, XXREAL_0, TARSKI, CARD_1, SUPINF_2, MSSUBFAM, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, RLSUB_1, BINOP_1, ZFMISC_1, INT_1, RLVECT_2, ZMODUL01, ZMODUL03, RLVECT_3, RMOD_2, RANKNULL, UNIALG_1, MSAFREE2, INT_3, COMPLEX1, VECTSP_1, MESFUNC1, XCMPLX_0, REALSET1, VECTSP10, ZMODUL02, ZMODUL04, ZMODUL06, ZMODUL07, ZMODUL08;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, RAT_1, BINOP_2, REALSET1, EQREL_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, INT_3, MOD_2, ZMODUL01, ZMODUL02, ZMODUL03, GAUSSINT, ZMODUL04, ZMODUL05, ZMODUL06, ZMODUL07;
definitions TARSKI, VECTSP_1;
theorems CARD_1, CARD_2, FUNCT_1, FUNCT_2, INT_1, RLVECT_1, TARSKI, ZMODUL01, BINOP_2, ZFMISC_1, RELAT_1, GAUSSINT, EC_PF_1, ZMODUL03, XBOOLE_0, XBOOLE_1, XCMPLX_1, ORDINAL1, VECTSP_7, VECTSP_1, ALGSTR_0, INT_2, ZMODUL02, NAT_D, NUMBERS, EQREL_1, VECTSP_6, RAT_1, ABSVALUE, COMPLEX1, VECTSP_4, ZMODUL04, ZMODUL05, ZMODUL06, ZMODUL07;
schemes FUNCT_2, NAT_1, XBOOLE_0;
registrations SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, STRUCT_0, RLVECT_1, MEMBERED, CARD_1, INT_1, XBOOLE_0, ORDINAL1, XXREAL_0, NAT_1, INT_3, REALSET1, RELAT_1, VECTSP_1, GAUSSINT, VECTSP_7, EQREL_1, RAT_1, XCMPLX_0, ZMODUL03, ZMODUL04, ZMODUL06, ZMODUL07;
constructors HIDDEN, BINOP_2, UPROOTS, ZMODUL01, REALSET1, ALGSTR_1, EC_PF_1, ZMODUL04, ZMODUL06, ZMODUL07;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XCMPLX_0, BINOP_1, STRUCT_0, ALGSTR_0, INT_3, VECTSP_1, ZMODUL02, REALSET1, GAUSSINT, VECTSP_4, VECTSP_6, ZMODUL07;
expansions TARSKI, STRUCT_0, ALGSTR_0, VECTSP_1, VECTSP_5, ZMODUL06, MOD_2;
LMLT12:
addreal || INT = addint