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 A1: ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
then lim ||.(seq + (- x)).|| = ||.(g + (- x)).|| by Lm1;
then A2: lim ||.(seq - x).|| = ||.(g + (- x)).|| by BHSP_1:56;
||.(seq + (- x)).|| is convergent by A1, Lm1;
hence ( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| ) by A2, BHSP_1:56, RLVECT_1:def 11; :: thesis: verum