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).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
let g, x be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| ) )
assume that
A1: seq is convergent and
A2: lim seq = g ; :: thesis: ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
A3: seq + x is convergent by A1, Th7;
lim (seq + x) = g + x by A1, A2, Th17;
hence ( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| ) by A3, Th21; :: thesis: verum