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 ( seq is convergent & lim seq = g ) ; :: thesis: ( dist (seq + x),(g + x) is convergent & lim (dist (seq + x),(g + x)) = 0 )
then ( seq + x is convergent & lim (seq + x) = g + x ) by Th7, Th17;
hence ( dist (seq + x),(g + x) is convergent & lim (dist (seq + x),(g + x)) = 0 ) by Th24; :: thesis: verum