let CNS be ComplexNormSpace; :: thesis: for x being Point of CNS
for S being sequence of CNS st S is convergent holds
lim (S - x) = (lim S) - x
let x be Point of CNS; :: thesis: for S being sequence of CNS st S is convergent holds
lim (S - x) = (lim S) - x
let S be sequence of CNS; :: 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, Def16;
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) - H1(CNS)) - (lim S)).|| by RLVECT_1:13
.= ||.(((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, NORMSP_1:def 4; :: thesis: verum
end;
S - x is convergent by A1, Th115;
hence lim (S - x) = (lim S) - x by A2, Def16; :: thesis: verum