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

hence lim (seq + x) = (lim seq) + x by A2, Def2; :: 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 )

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

seq + x is convergent
by A1, Th7;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;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

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