environ
vocabularies HIDDEN, ARYTM_3, POLYNOM2, COMPLFLD, POLYNOM1, ARYTM_1, FUNCT_1, REAL_1, COMPLEX1, POLYNOM3, RELAT_1, RLVECT_1, FINSEQ_1, ZFMISC_1, INT_1, VECTSP_1, ALGSEQ_1, GROUP_1, ALGSTR_1, POLYNOM5, SGRAPH1, ALGSTR_0, FUNCT_4, RATFUNC1, MCART_1, HURWITZ, HURWITZ2, XBOOLE_0, POLYNOM4, BINOP_1, PARTFUN1, LATTICES, XREAL_0, ABIAN, XCMPLX_0, SQUARE_1, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, NUMBERS, CARD_1, MESFUNC1, XXREAL_0, VALUED_0, YELLOW_8;
notations HIDDEN, TARSKI, SUBSET_1, VALUED_0, NUMBERS, ORDINAL1, XCMPLX_0, COMPLEX1, COMPLFLD, XREAL_0, SQUARE_1, RELAT_1, ALGSTR_0, FUNCT_7, VECTSP_1, ARYTM_3, FUNCT_1, FUNCT_2, NAT_1, NAT_D, INT_1, GROUP_1, ABIAN, BINOP_1, XXREAL_0, STRUCT_0, ALGSTR_1, RLVECT_1, VFUNCT_1, NORMSP_1, ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5, RATFUNC1, HURWITZ;
definitions FINSEQ_1, POLYNOM3, STRUCT_0, ALGSTR_0, VECTSP_1, SQUARE_1, ARYTM_3, XREAL_0, XXREAL_0, XCMPLX_0, ALGSTR_1, COMPLFLD, ALGSEQ_1, HURWITZ, BHSP_1, VFUNCT_1, RATFUNC1;
theorems VECTSP_1, ALGSEQ_1, FUNCT_1, FUNCT_2, POLYNOM3, FUNCOP_1, RLVECT_1, POLYNOM4, GROUP_1, TARSKI, RATFUNC1, HURWITZ, INT_1, COMPLFLD, POLYNOM5, ALGSTR_1, COMPLEX1, FUNCT_7, NAT_1, BHSP_1, NORMSP_1, ORDINAL1, XREAL_0, VALUED_0, XREAL_1, XXREAL_0, ABIAN, XCMPLX_1, SQUARE_1;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, INT_1, NAT_1, MEMBERED, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1, POLYNOM4, POLYNOM5, XREAL_0, VALUED_0, ABIAN, FUNCT_2, RATFUNC1, POLYNOM3, VFUNCT_1, XTUPLE_0;
constructors HIDDEN, BINOP_1, REAL_1, BINARITH, ALGSTR_1, POLYNOM5, BHSP_1, RELSET_1, FUNCT_4, ARYTM_3, ABIAN, NAT_D, SQUARE_1, POLYNOM4, VFUNCT_1, RATFUNC1, HURWITZ, ALGSEQ_1, BINOP_2, XXREAL_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_1, POLYNOM3, STRUCT_0, ALGSTR_0, VECTSP_1, SQUARE_1, ARYTM_3, XREAL_0, XXREAL_0, XCMPLX_0, ALGSTR_1, COMPLFLD, ALGSEQ_1, HURWITZ, BHSP_1, VFUNCT_1, RATFUNC1;
expansions FINSEQ_1, POLYNOM3, STRUCT_0, ALGSTR_0, VECTSP_1, SQUARE_1, ARYTM_3, XREAL_0, XXREAL_0, XCMPLX_0, ALGSTR_1, COMPLFLD, ALGSEQ_1, HURWITZ, BHSP_1, VFUNCT_1, RATFUNC1;
Lm1:
(2 * 0) + 1 = 1
;