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) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
let x, g be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 ) )
assume A1: ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
then lim ||.((seq + (- x)) - (g + (- x))).|| = 0 by Th33;
then A2: lim ||.((seq - x) - (g + (- x))).|| = 0 by BHSP_1:56;
||.((seq + (- x)) - (g + (- x))).|| is convergent by A1, Th33;
then ||.((seq - x) - (g + (- x))).|| is convergent by BHSP_1:56;
hence ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 ) by A2, RLVECT_1:def 11; :: thesis: verum