environ
vocabularies HIDDEN, NUMBERS, CSSPACE, PRE_TOPC, XCMPLX_0, REAL_1, NAT_1, SUBSET_1, ORDINAL2, SUPINF_2, SEQ_2, XXREAL_0, CARD_1, METRIC_1, FUNCT_1, ARYTM_3, ARYTM_1, RELAT_1, COMPLEX1, NORMSP_1, SEQ_1, TARSKI, STRUCT_0, XBOOLE_0, BHSP_3, XXREAL_2, VALUED_0, REWRITE1;
notations HIDDEN, TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, NAT_1, SEQ_1, VALUED_0, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_1, BHSP_1, SEQ_2, CLVECT_1, CSSPACE, RECDEF_1;
definitions ;
theorems XBOOLE_0, TARSKI, ABSVALUE, SEQ_2, SEQM_3, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, XCMPLX_0, XBOOLE_1, CLVECT_1, COMPLEX1, NORMSP_1, CSSPACE, SUBSET_1, XREAL_1, XXREAL_0, ORDINAL1, BHSP_1, VALUED_0;
schemes SEQ_1, FRAENKEL, NAT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, MEMBERED, STRUCT_0, VALUED_0, VFUNCT_1, FUNCT_2;
constructors HIDDEN, REAL_1, COMPLEX1, SEQ_2, BHSP_3, CSSPACE, VALUED_1, RECDEF_1, RELSET_1, VFUNCT_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities ;
expansions ;
deffunc H1( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;
Lm1:
for X being ComplexUnitarySpace
for x, g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
deffunc H2( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;