let s2, s1 be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds 0 <= s2 . n ) & s1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
s2 . n <= s1 . n implies s2 is summable )
assume that
A1: for n being Element of NAT holds 0 <= s2 . n and
A2: s1 is summable ; :: thesis: ( for m being Element of NAT ex n being Element of NAT st
( m <= n & not s2 . n <= s1 . n ) or s2 is summable )
given m being Element of NAT such that A3: for n being Element of NAT st m <= n holds
s2 . n <= s1 . n ; :: thesis: s2 is summable

A4: now

let n be Element of NAT ; :: thesis: 0 <= (s1 ^\ m) . n
A5: (s1 ^\ m) . n = s1 . (n + m) by NAT_1:def 3;
0 <= s2 . (n + m) by A1;
hence 0 <= (s1 ^\ m) . n by A3, A5, NAT_1:11; :: thesis: verum

end;

s1 ^\ m is summable by A2, Th15;
then Partial_Sums (s1 ^\ m) is bounded_above by A4, Th20;
then consider r being real number such that
A6: for n being Element of NAT holds (Partial_Sums (s1 ^\ m)) . n < r by SEQ_2:def 3;

A7: now

let n be Element of NAT ; :: thesis: (s2 ^\ m) . n <= (s1 ^\ m) . n
s2 . (n + m) <= s1 . (n + m) by A3, NAT_1:12;
then (s2 ^\ m) . n <= s1 . (n + m) by NAT_1:def 3;
hence (s2 ^\ m) . n <= (s1 ^\ m) . n by NAT_1:def 3; :: thesis: verum

end;

A8: now

let n be Element of NAT ; :: thesis: 0 <= (s2 ^\ m) . n
(s2 ^\ m) . n = s2 . (n + m) by NAT_1:def 3;
hence 0 <= (s2 ^\ m) . n by A1; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: (Partial_Sums (s2 ^\ m)) . n < r
(Partial_Sums (s2 ^\ m)) . n <= (Partial_Sums (s1 ^\ m)) . n by A7, Th17;
hence (Partial_Sums (s2 ^\ m)) . n < r by A6, XXREAL_0:2; :: thesis: verum

end;

then Partial_Sums (s2 ^\ m) is bounded_above by SEQ_2:def 3;
then s2 ^\ m is summable by A8, Th20;
hence s2 is summable by Th16; :: thesis: verum