begin
deffunc H1( RealUnitarySpace) -> Element of the carrier of $1 = 0. $1;
Lm1:
for X being RealUnitarySpace
for g, x 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).|| )