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 ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )

then ( seq + x is convergent & lim (seq + x) = g + x ) by Th7, Th17;

hence ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 ) by Th22; :: 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 ( seq is convergent & lim seq = g ) ; :: thesis: ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )

then ( seq + x is convergent & lim (seq + x) = g + x ) by Th7, Th17;

hence ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 ) by Th22; :: thesis: verum