let X be RealUnitarySpace; :: thesis: for x being Point of X

for seq being sequence of X st seq is convergent holds

lim (seq - x) = (lim seq) - x

let x be Point of X; :: thesis: for seq being sequence of X st seq is convergent holds

lim (seq - x) = (lim seq) - x

let seq be sequence of X; :: thesis: ( seq is convergent implies lim (seq - x) = (lim seq) - x )

assume seq is convergent ; :: thesis: lim (seq - x) = (lim seq) - x

then lim (seq + (- x)) = (lim seq) + (- x) by Th17;

then lim (seq - x) = (lim seq) + (- x) by BHSP_1:56;

hence lim (seq - x) = (lim seq) - x by RLVECT_1:def 11; :: thesis: verum

for seq being sequence of X st seq is convergent holds

lim (seq - x) = (lim seq) - x

let x be Point of X; :: thesis: for seq being sequence of X st seq is convergent holds

lim (seq - x) = (lim seq) - x

let seq be sequence of X; :: thesis: ( seq is convergent implies lim (seq - x) = (lim seq) - x )

assume seq is convergent ; :: thesis: lim (seq - x) = (lim seq) - x

then lim (seq + (- x)) = (lim seq) + (- x) by Th17;

then lim (seq - x) = (lim seq) + (- x) by BHSP_1:56;

hence lim (seq - x) = (lim seq) - x by RLVECT_1:def 11; :: thesis: verum