let X be RealUnitarySpace; :: thesis: 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).|| )
let x, g be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| ) )
assume ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
then ( seq + x is convergent & lim (seq + x) = g + x ) by Th7, Th17;
hence ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| ) by Th21; :: thesis: verum