let s1, s2 be Real_Sequence; :: thesis: ( ( for n being Nat holds

( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable implies ( s1 is summable & Sum s1 <= Sum s2 ) )

assume that

A1: for n being Nat holds

( 0 <= s1 . n & s1 . n <= s2 . n ) and

A2: s2 is summable ; :: thesis: ( s1 is summable & Sum s1 <= Sum s2 )

for n being Nat st 0 <= n holds

s1 . n <= s2 . n by A1;

hence s1 is summable by A1, A2, Th19; :: thesis: Sum s1 <= Sum s2

then A3: Partial_Sums s1 is convergent ;

( Partial_Sums s2 is convergent & ( for n being Nat holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n ) ) by A1, A2, Th14;

hence Sum s1 <= Sum s2 by A3, SEQ_2:18; :: thesis: verum

( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable implies ( s1 is summable & Sum s1 <= Sum s2 ) )

assume that

A1: for n being Nat holds

( 0 <= s1 . n & s1 . n <= s2 . n ) and

A2: s2 is summable ; :: thesis: ( s1 is summable & Sum s1 <= Sum s2 )

for n being Nat st 0 <= n holds

s1 . n <= s2 . n by A1;

hence s1 is summable by A1, A2, Th19; :: thesis: Sum s1 <= Sum s2

then A3: Partial_Sums s1 is convergent ;

( Partial_Sums s2 is convergent & ( for n being Nat holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n ) ) by A1, A2, Th14;

hence Sum s1 <= Sum s2 by A3, SEQ_2:18; :: thesis: verum