let X be ComplexUnitarySpace; :: 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 that
A1: seq is convergent and
A2: lim seq = g ; :: thesis: ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )
A3: seq + x is convergent by A1, Th7;
lim (seq + x) = g + x by A1, A2, Th17;
hence ( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 ) by A3, Th22; :: thesis: verum