let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: 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 ) )
let seq be ExtREAL_sequence; :: thesis: 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 ) )
let n, m be Nat; :: thesis: ( ( ( 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 ) )

hereby :: thesis: ( ( for i, j being Nat holds f . (i,j) <= seq . j ) implies (Partial_Sums_in_cod2 f) . (n,m) <= (Partial_Sums seq) . m )

assume A1: for i, j being Nat holds f . (i,j) <= seq . i ; :: thesis: (Partial_Sums_in_cod1 f) . (n,m) <= (Partial_Sums seq) . n
defpred S₁[ Nat] means (Partial_Sums_in_cod1 f) . ($1,m) <= (Partial_Sums seq) . $1;
A2: (Partial_Sums_in_cod1 f) . (0,m) = f . (0,m) by DefRSM;
(Partial_Sums seq) . 0 = seq . 0 by MESFUNC9:def 1;
then A3: S₁[ 0 ] by A1, A2;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
A6: f . ((k + 1),m) <= seq . (k + 1) by A1;
A7: (Partial_Sums_in_cod1 f) . ((k + 1),m) = ((Partial_Sums_in_cod1 f) . (k,m)) + (f . ((k + 1),m)) by DefRSM;
(Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by MESFUNC9:def 1;
hence S₁[k + 1] by A5, A6, A7, XXREAL_3:36; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence (Partial_Sums_in_cod1 f) . (n,m) <= (Partial_Sums seq) . n ; :: thesis: verum

end;

assume A1: for i, j being Nat holds f . (i,j) <= seq . j ; :: thesis: (Partial_Sums_in_cod2 f) . (n,m) <= (Partial_Sums seq) . m
defpred S₁[ Nat] means (Partial_Sums_in_cod2 f) . (n,$1) <= (Partial_Sums seq) . $1;
A2: (Partial_Sums_in_cod2 f) . (n,0) = f . (n,0) by DefCSM;
(Partial_Sums seq) . 0 = seq . 0 by MESFUNC9:def 1;
then A3: S₁[ 0 ] by A1, A2;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
A6: f . (n,(k + 1)) <= seq . (k + 1) by A1;
A7: (Partial_Sums_in_cod2 f) . (n,(k + 1)) = ((Partial_Sums_in_cod2 f) . (n,k)) + (f . (n,(k + 1))) by DefCSM;
(Partial_Sums seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by MESFUNC9:def 1;
hence S₁[k + 1] by A5, A6, A7, XXREAL_3:36; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence (Partial_Sums_in_cod2 f) . (n,m) <= (Partial_Sums seq) . m ; :: thesis: verum