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 )
set g = lim seq;
assume A1: seq is convergent ; :: thesis: lim (seq + x) = (lim seq) + x

A2: now :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < r

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n being Nat st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < r
then consider m1 being Nat such that
A3: for n being Nat st n >= m1 holds
dist ((seq . n),(lim seq)) < r by A1, Def2;
take k = m1; :: thesis: for n being Nat st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < r
let n be Nat; :: thesis: ( n >= k implies dist (((seq + x) . n),((lim seq) + x)) < r )
assume n >= k ; :: thesis: dist (((seq + x) . n),((lim seq) + x)) < r
then A4: dist ((seq . n),(lim seq)) < r by A3;
dist ((seq . n),(lim seq)) = dist (((seq . n) - (- x)),((lim seq) - (- x))) by BHSP_1:42
.= dist (((seq . n) + (- (- x))),((lim seq) - (- x))) by RLVECT_1:def 11
.= dist (((seq . n) + x),((lim seq) - (- x))) by RLVECT_1:17
.= dist (((seq . n) + x),((lim seq) + (- (- x)))) by RLVECT_1:def 11
.= dist (((seq . n) + x),((lim seq) + x)) by RLVECT_1:17 ;
hence dist (((seq + x) . n),((lim seq) + x)) < r by A4, BHSP_1:def 6; :: thesis: verum

end;

seq + x is convergent by A1, Th7;
hence lim (seq + x) = (lim seq) + x by A2, Def2; :: thesis: verum