let X be RealUnitarySpace; :: thesis: for g, x 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 g, x 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 ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
then ( ||.((seq + (- x)) - (g + (- x))).|| is convergent & lim ||.((seq + (- x)) - (g + (- x))).|| = 0 ) by Th33;
then ( ||.((seq - x) - (g + (- x))).|| is convergent & lim ||.((seq - x) - (g + (- x))).|| = 0 ) by BHSP_1:78;
hence ( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 ) by RLVECT_1:def 12; :: thesis: verum