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)
A3: S1 - S2 is convergent by A1, A2, Th35;
set g1 = lim S1;
set g2 = lim S2;
set g = (lim S1) - (lim S2);

now

let r be Real; :: thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r )
assume 0 < r ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
then A4: 0 < r / 2 by XREAL_1:217;
then consider m1 being Element of NAT such that
A5: for n being Element of NAT st m1 <= n holds
||.((S1 . n) - (lim S1)).|| < r / 2 by A1, Def11;
consider m2 being Element of NAT such that
A6: for n being Element of NAT st m2 <= n holds
||.((S2 . n) - (lim S2)).|| < r / 2 by A2, A4, Def11;
take k = m1 + m2; :: thesis: for n being Element of NAT st k <= n holds
||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r
let n be Element of 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
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A7, XXREAL_0:2;
then A8: ||.((S1 . n) - (lim S1)).|| < r / 2 by A5;
m2 <= k by NAT_1:12;
then m2 <= n by A7, XXREAL_0:2;
then ||.((S2 . n) - (lim S2)).|| < r / 2 by A6;
then A9: ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| < (r / 2) + (r / 2) by A8, XREAL_1:10;
A10: ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| = ||.(((S1 . n) - (S2 . n)) - ((lim S1) - (lim S2))).|| by Def6
.= ||.((((S1 . n) - (S2 . n)) - (lim S1)) + (lim S2)).|| by RLVECT_1:43
.= ||.(((S1 . n) - ((lim S1) + (S2 . n))) + (lim S2)).|| by RLVECT_1:41
.= ||.((((S1 . n) - (lim S1)) - (S2 . n)) + (lim S2)).|| by RLVECT_1:41
.= ||.(((S1 . n) - (lim S1)) - ((S2 . n) - (lim S2))).|| by RLVECT_1:43 ;
||.(((S1 . n) - (lim S1)) - ((S2 . n) - (lim S2))).|| <= ||.((S1 . n) - (lim S1)).|| + ||.((S2 . n) - (lim S2)).|| by Th7;
hence ||.(((S1 - S2) . n) - ((lim S1) - (lim S2))).|| < r by A9, A10, XXREAL_0:2; :: thesis: verum

end;

hence lim (S1 - S2) = (lim S1) - (lim S2) by A3, Def11; :: thesis: verum