let RNS be RealNormSpace; :: thesis: for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
lim (S1 - S2) = (lim S1) - (lim S2)
let S1, S2 be sequence of RNS; :: thesis: ( S1 is convergent & S2 is convergent implies lim (S1 - S2) = (lim S1) - (lim S2) )
assume that
A1: S1 is convergent and
A2: S2 is convergent ; :: thesis: lim (S1 - S2) = (lim S1) - (lim S2)
set g2 = lim S2;
set g1 = lim S1;
set g = (lim S1) - (lim S2);

A3: now :: thesis: for r being Real st 0 < r holds
ex k being set st
for n being Nat st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r

let r be Real; :: thesis: ( 0 < r implies ex k being set st
for n being Nat st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r )
assume 0 < r ; :: thesis: ex k being set st
for n being Nat st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
then A4: 0 < r / 2 ;
then consider m1 being Nat such that
A5: for n being Nat st m1 <= n holds
||.((S1 . n) - (lim S1)).|| < r / 2 by A1, Def7;
consider m2 being Nat such that
A6: for n being Nat st m2 <= n holds
||.((S2 . n) - (lim S2)).|| < r / 2 by A2, A4, Def7;
take k = m1 + m2; :: thesis: for n being Nat st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
let n be Nat; :: thesis: ( k <= n implies ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r )
assume A7: k <= n ; :: thesis: ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
m2 <= k by NAT_1:12;
then m2 <= n by A7, XXREAL_0:2;
then A8: ||.((S2 . n) - (lim S2)).|| < r / 2 by A6;
A9: ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| = ||.(((S1 . n) - (S2 . n)) - ((lim S1) - (lim S2))).|| by Def3
.= ||.((((S1 . n) - (S2 . n)) - (lim S1)) + (lim S2)).|| by RLVECT_1:29
.= ||.(((S1 . n) - ((lim S1) + (S2 . n))) + (lim S2)).|| by RLVECT_1:27
.= ||.((((S1 . n) - (lim S1)) - (S2 . n)) + (lim S2)).|| by RLVECT_1:27
.= ||.(((S1 . n) - (lim S1)) - ((S2 . n) - (lim S2))).|| by RLVECT_1:29 ;
A10: ||.(((S1 . n) - (lim S1)) - ((S2 . n) - (lim S2))).|| <= ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| by Th3;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A7, XXREAL_0:2;
then ||.((S1 . n) - (lim S1)).|| < r / 2 by A5;
then ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| < (r / 2) + (r / 2) by A8, XREAL_1:8;
hence ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r by A9, A10, XXREAL_0:2; :: thesis: verum

end;

S1 - S2 is convergent by A1, A2, Th20;
hence lim (S1 - S2) = (lim S1) - (lim S2) by A3, Def7; :: thesis: verum