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