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;

hence s2 is summable by Th13; :: thesis: verum

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;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

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

then A6:
Partial_Sums (s2 ^\ m) is bounded_above
by SEQ_2:def 3;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;(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

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

then
s2 ^\ m is summable
by A6, Th17;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;(s2 ^\ m) . n = s2 . (n + m) by NAT_1:def 3;

hence 0 <= (s2 ^\ m) . n by A1; :: thesis: verum

hence s2 is summable by Th13; :: thesis: verum