environ
vocabularies HIDDEN, NUMBERS, REAL_1, SEQ_1, SUBSET_1, BHSP_1, SUPINF_2, XBOOLE_0, ALGSTR_0, NAT_1, SERIES_1, FUNCT_1, CARD_1, ARYTM_3, PRE_TOPC, STRUCT_0, RLVECT_1, ARYTM_1, RELAT_1, SEQ_2, CARD_3, ORDINAL2, BHSP_3, XXREAL_0, NORMSP_1, XXREAL_2, FUNCOP_1, COMPLEX1, VALUED_1, POWER, NEWTON, VALUED_0, INT_1, METRIC_1, RSSPACE2;
notations HIDDEN, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, ALGSTR_0, REAL_1, INT_1, NAT_1, FUNCT_2, FUNCOP_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, VALUED_0, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_1, BHSP_1, BHSP_2, BHSP_3, RSSPACE2, NEWTON, POWER, XXREAL_0;
definitions FUNCT_2;
theorems NAT_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SERIES_1, ABSVALUE, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, PREPOWER, POWER, INT_1, NORMSP_1, XCMPLX_1, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1;
schemes NAT_1, FUNCT_2;
registrations ORDINAL1, RELSET_1, XREAL_0, INT_1, MEMBERED, STRUCT_0, RLVECT_1, VALUED_0, VALUED_1, FUNCT_2, NUMBERS, FUNCOP_1, VFUNCT_1, BHSP_2, BHSP_3, NEWTON, NAT_1;
constructors HIDDEN, REAL_1, SEQ_2, NEWTON, SERIES_1, BHSP_2, BHSP_3, RELSET_1, ABIAN, BINOP_2, VFUNCT_1, COMSEQ_2;
requirements HIDDEN, NUMERALS, REAL, SUBSET, ARITHM, BOOLE;
equalities RLVECT_1, SERIES_1, VALUED_1;
expansions FUNCT_2, VALUED_1;
deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;