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