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

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