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