environ
vocabularies HIDDEN, NUMBERS, BHSP_1, PRE_TOPC, REAL_1, NAT_1, SUBSET_1, SUPINF_2, SEQ_2, XXREAL_0, CARD_1, METRIC_1, FUNCT_1, ARYTM_3, ARYTM_1, RELAT_1, COMPLEX1, NORMSP_1, ORDINAL2, SEQ_1, TARSKI, STRUCT_0, XBOOLE_0;
notations HIDDEN, TARSKI, ORDINAL1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, SEQ_1, COMSEQ_2, SEQ_2, RELAT_1, VALUED_0, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, BHSP_1, NORMSP_1, XXREAL_0;
definitions ;
theorems TARSKI, NAT_1, FUNCT_1, SEQ_2, ABSVALUE, SUBSET_1, RLVECT_1, BHSP_1, NORMSP_1, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XREAL_1, COMPLEX1, XXREAL_0, VALUED_0, ORDINAL1;
schemes SEQ_1, FRAENKEL;
registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, VFUNCT_1, FUNCT_2, NAT_1;
constructors HIDDEN, DOMAIN_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, SEQ_2, BHSP_1, VALUED_1, RELSET_1, VFUNCT_1, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions ;
deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;
Lm1:
for X being RealUnitarySpace
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).|| )