environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, NORMSP_1, PARTFUN1, NAT_1, PRE_TOPC, XBOOLE_0, ALGSTR_0, ARYTM_1, ARYTM_3, FUNCT_1, RELAT_1, STRUCT_0, RCOMP_1, CARD_1, TARSKI, XXREAL_0, SUPINF_2, VALUED_0, SEQ_2, ORDINAL2, FCONT_1, FUNCT_2, COMPLEX1, VALUED_1, CFCONT_1, SEQ_1, SEQ_4, NFCONT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, PARTFUN2, FUNCT_2, PRE_TOPC, VALUED_0, STRUCT_0, ALGSTR_0, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, REAL_1, XREAL_0, RLVECT_1, SEQ_1, SEQ_2, SEQ_4, RCOMP_1, VFUNCT_1, NORMSP_0, NORMSP_1, XXREAL_0;
definitions TARSKI;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, XCMPLX_0, XCMPLX_1, ZFMISC_1, RCOMP_1, SEQ_2, RELAT_1, FUNCT_1, VFUNCT_1, LOPBAN_1, FUNCT_2, SEQ_4, NORMSP_1, PARTFUN1, PARTFUN2, XREAL_1, COMPLEX1, XXREAL_0, BHSP_1, VALUED_0, NORMSP_0, ORDINAL1;
schemes FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, NAT_1, STRUCT_0, RLVECT_1, VALUED_0, XREAL_0, VFUNCT_1, FUNCT_2;
constructors HIDDEN, REAL_1, COMPLEX1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2, VFUNCT_1, RELSET_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1, RELAT_1;
expansions TARSKI;
reconsider jj = 1 as Real ;