let S be Real_Sequence; :: thesis: for x being Real st S is convergent holds

( S - x is convergent & lim (S - x) = (lim S) - x )

let x be Real; :: thesis: ( S is convergent implies ( S - x is convergent & lim (S - x) = (lim S) - x ) )

assume B1: S is convergent ; :: thesis: ( S - x is convergent & lim (S - x) = (lim S) - x )

set g = lim S;

set h = (lim S) - x;

hence lim (S - x) = (lim S) - x by X1, SEQ_2:def 7; :: thesis: verum

( S - x is convergent & lim (S - x) = (lim S) - x )

let x be Real; :: thesis: ( S is convergent implies ( S - x is convergent & lim (S - x) = (lim S) - x ) )

assume B1: S is convergent ; :: thesis: ( S - x is convergent & lim (S - x) = (lim S) - x )

set g = lim S;

set h = (lim S) - x;

X1: now :: thesis: for r being Real st 0 < r holds

ex k being Nat st

for n being Nat st k <= n holds

|.(((S - x) . n) - ((lim S) - x)).| < r

hence
S - x is convergent
; :: thesis: lim (S - x) = (lim S) - xex k being Nat st

for n being Nat st k <= n holds

|.(((S - x) . n) - ((lim S) - x)).| < r

let r be Real; :: thesis: ( 0 < r implies ex k being Nat st

for n being Nat st k <= n holds

|.(((S - x) . n) - ((lim S) - x)).| < r )

assume 0 < r ; :: thesis: ex k being Nat st

for n being Nat st k <= n holds

|.(((S - x) . n) - ((lim S) - x)).| < r

then consider m1 being Nat such that

A2: for n being Nat st m1 <= n holds

|.((S . n) - (lim S)).| < r by B1, SEQ_2:def 7;

take k = m1; :: thesis: for n being Nat st k <= n holds

|.(((S - x) . n) - ((lim S) - x)).| < r

let n be Nat; :: thesis: ( k <= n implies |.(((S - x) . n) - ((lim S) - x)).| < r )

assume B3: k <= n ; :: thesis: |.(((S - x) . n) - ((lim S) - x)).| < r

|.((S . n) - (lim S)).| = |.(((S . n) - x) - ((lim S) - x)).|

.= |.(((S - x) . n) - ((lim S) - x)).| by Def14 ;

hence |.(((S - x) . n) - ((lim S) - x)).| < r by A2, B3; :: thesis: verum

end;for n being Nat st k <= n holds

|.(((S - x) . n) - ((lim S) - x)).| < r )

assume 0 < r ; :: thesis: ex k being Nat st

for n being Nat st k <= n holds

|.(((S - x) . n) - ((lim S) - x)).| < r

then consider m1 being Nat such that

A2: for n being Nat st m1 <= n holds

|.((S . n) - (lim S)).| < r by B1, SEQ_2:def 7;

take k = m1; :: thesis: for n being Nat st k <= n holds

|.(((S - x) . n) - ((lim S) - x)).| < r

let n be Nat; :: thesis: ( k <= n implies |.(((S - x) . n) - ((lim S) - x)).| < r )

assume B3: k <= n ; :: thesis: |.(((S - x) . n) - ((lim S) - x)).| < r

|.((S . n) - (lim S)).| = |.(((S . n) - x) - ((lim S) - x)).|

.= |.(((S - x) . n) - ((lim S) - x)).| by Def14 ;

hence |.(((S - x) . n) - ((lim S) - x)).| < r by A2, B3; :: thesis: verum

hence lim (S - x) = (lim S) - x by X1, SEQ_2:def 7; :: thesis: verum