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;

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

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;

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