let RNS be RealNormSpace; :: thesis: for x being Point of RNS
for S being sequence of RNS st S is convergent holds
S - x is convergent
let x be Point of RNS; :: thesis: for S being sequence of RNS st S is convergent holds
S - x is convergent
let S be sequence of RNS; :: thesis: ( S is convergent implies S - x is convergent )
assume S is convergent ; :: thesis: S - x is convergent
then consider g being Point of RNS such that
A1: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r ;
take h = g - x; :: according to NORMSP_1:def 6 :: thesis: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.(((S - x) . n) - h).|| < r
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.(((S - x) . n) - h).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.(((S - x) . n) - h).|| < r
then consider m1 being Nat such that
A2: for n being Nat st m1 <= n holds
||.((S . n) - g).|| < r by A1;
take k = m1; :: thesis: for n being Nat st k <= n holds
||.(((S - x) . n) - h).|| < r
let n be Nat; :: thesis: ( k <= n implies ||.(((S - x) . n) - h).|| < r )
assume k <= n ; :: thesis: ||.(((S - x) . n) - h).|| < r
then A3: ||.((S . n) - g).|| < r by A2;
||.((S . n) - g).|| = ||.(((S . n) - H₁(RNS)) - g).||
.= ||.(((S . n) - (x - x)) - g).|| by RLVECT_1:15
.= ||.((((S . n) - x) + x) - g).|| by RLVECT_1:29
.= ||.(((S . n) - x) + ((- g) + x)).|| by RLVECT_1:def 3
.= ||.(((S . n) - x) - h).|| by RLVECT_1:33 ;
hence ||.(((S - x) . n) - h).|| < r by A3, Def4; :: thesis: verum