let RNS be RealNormSpace; :: thesis: for x being Point of RNS
for S being sequence of RNS st S is convergent holds
lim (S - x) = (lim S) - x
let x be Point of RNS; :: thesis: for S being sequence of RNS st S is convergent holds
lim (S - x) = (lim S) - x
let S be sequence of RNS; :: thesis: ( S is convergent implies lim (S - x) = (lim S) - x )
set g = lim S;
set h = (lim S) - x;
assume A1: S is convergent ; :: thesis: lim (S - x) = (lim S) - x

A2: 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
A3: for n being Nat st m1 <= n holds
||.((S . n) - (lim S)).|| < r by A1, Def7;
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 k <= n ; :: thesis: ||.(((S - x) . n) - ((lim S) - x)).|| < r
then A4: ||.((S . n) - (lim S)).|| < r by A3;
||.((S . n) - (lim S)).|| = ||.(((S . n) - H₁(RNS)) - (lim S)).||
.= ||.(((S . n) - (x - x)) - (lim S)).|| by RLVECT_1:15
.= ||.((((S . n) - x) + x) - (lim S)).|| by RLVECT_1:29
.= ||.(((S . n) - x) + ((- (lim S)) + x)).|| by RLVECT_1:def 3
.= ||.(((S . n) - x) - ((lim S) - x)).|| by RLVECT_1:33 ;
hence ||.(((S - x) . n) - ((lim S) - x)).|| < r by A4, Def4; :: thesis: verum

end;

S - x is convergent by A1, Th21;
hence lim (S - x) = (lim S) - x by A2, Def7; :: thesis: verum