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

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