let X be RealUnitarySpace; :: thesis: for x being Point of X
for seq being sequence of X st seq is convergent holds
seq - x is convergent
let x be Point of X; :: thesis: for seq being sequence of X st seq is convergent holds
seq - x is convergent
let seq be sequence of X; :: thesis: ( seq is convergent implies seq - x is convergent )
assume seq is convergent ; :: thesis: seq - x is convergent
then seq + (- x) is convergent by Th7;
hence seq - x is convergent by BHSP_1:56; :: thesis: verum