let s1, s2 be Real_Sequence; :: thesis: ( ( for n being Nat holds 0 <= s2 . n ) & s1 is summable & ex m being Nat st
for n being Nat st m <= n holds
s2 . n <= s1 . n implies s2 is summable )
assume that
A1: for n being Nat holds 0 <= s2 . n and
A2: s1 is summable ; :: thesis: ( for m being Nat ex n being Nat st
( m <= n & not s2 . n <= s1 . n ) or s2 is summable )
given m being Nat such that A3: for n being Nat st m <= n holds
s2 . n <= s1 . n ; :: thesis: s2 is summable
s1 ^\ m is summable by A2, Th12;
then Partial_Sums (s1 ^\ m) is bounded_above ;
then consider r being Real such that
A4: for n being Nat holds (Partial_Sums (s1 ^\ m)) . n < r by SEQ_2:def 3;

A5: now :: thesis: for n being Nat holds (s2 ^\ m) . n <= (s1 ^\ m) . n

let n be 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;

now :: thesis: for n being Nat holds (Partial_Sums (s2 ^\ m)) . n < r

let n be Nat; :: thesis: (Partial_Sums (s2 ^\ m)) . n < r
(Partial_Sums (s2 ^\ m)) . n <= (Partial_Sums (s1 ^\ m)) . n by A5, Th14;
hence (Partial_Sums (s2 ^\ m)) . n < r by A4, XXREAL_0:2; :: thesis: verum

end;

then A6: Partial_Sums (s2 ^\ m) is bounded_above by SEQ_2:def 3;

now :: thesis: for n being Nat holds 0 <= (s2 ^\ m) . n

let n be 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;

then s2 ^\ m is summable by A6, Th17;
hence s2 is summable by Th13; :: thesis: verum