for f being Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence
for n, m being Nat holds
( ( ( for i, j being Nat holds f . (i,j) <= seq . i ) implies (Partial_Sums_in_cod1 f) . (n,m) <= (Partial_Sums seq) . n ) & ( ( for i, j being Nat holds f . (i,j) <= seq . j ) implies (Partial_Sums_in_cod2 f) . (n,m) <= (Partial_Sums seq) . m ) )