let s1, s2 be Real_Sequence; :: thesis: ( ( for n being Element of 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 Element of 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 Element of NAT st 0 <= n holds
s1 . n <= s2 . n by A1;
hence s1 is summable by A1, A2, Th22; :: thesis: Sum s1 <= Sum s2
then A3: Partial_Sums s1 is convergent by Def2;
A4: Partial_Sums s2 is convergent by A2, Def2;
for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n by A1, Th17;
hence Sum s1 <= Sum s2 by A3, A4, SEQ_2:32; :: thesis: verum