let f be without-infty Function of [:NAT,NAT:],ExtREAL; for n, m being Nat holds
( (Partial_Sums f) . ((n + 1),m) = ((Partial_Sums_in_cod2 f) . ((n + 1),m)) + ((Partial_Sums f) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m)) )
let n, m be Nat; ( (Partial_Sums f) . ((n + 1),m) = ((Partial_Sums_in_cod2 f) . ((n + 1),m)) + ((Partial_Sums f) . (n,m)) & (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m)) )
set RPS = Partial_Sums f;
set CPS = Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f);
set ROW = Partial_Sums_in_cod1 f;
set COL = Partial_Sums_in_cod2 f;
defpred S1[ Nat] means (Partial_Sums f) . ((n + 1),$1) = ((Partial_Sums_in_cod2 f) . ((n + 1),$1)) + ((Partial_Sums f) . (n,$1));
a1:
(Partial_Sums f) . (n,0) = (Partial_Sums_in_cod1 f) . (n,0)
by DefCSM;
(Partial_Sums f) . ((n + 1),0) =
(Partial_Sums_in_cod1 f) . ((n + 1),0)
by DefCSM
.=
((Partial_Sums_in_cod1 f) . (n,0)) + (f . ((n + 1),0))
by DefRSM
;
then a3:
S1[ 0 ]
by a1, DefCSM;
a4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
a6:
(Partial_Sums_in_cod2 f) . (
(n + 1),
(k + 1))
= ((Partial_Sums_in_cod2 f) . ((n + 1),k)) + (f . ((n + 1),(k + 1)))
by DefCSM;
X1:
(
(Partial_Sums_in_cod2 f) . (
(n + 1),
k)
<> -infty &
f . (
(n + 1),
(k + 1))
<> -infty &
(Partial_Sums f) . (
n,
k)
<> -infty &
(Partial_Sums_in_cod1 f) . (
n,
(k + 1))
<> -infty &
(Partial_Sums f) . (
(n + 1),
k)
<> -infty )
by MESFUNC5:def 5;
then X2:
((Partial_Sums_in_cod2 f) . ((n + 1),k)) + (f . ((n + 1),(k + 1))) <> -infty
by XXREAL_3:17;
(Partial_Sums f) . (
n,
(k + 1))
= ((Partial_Sums f) . (n,k)) + ((Partial_Sums_in_cod1 f) . (n,(k + 1)))
by DefCSM;
then ((Partial_Sums_in_cod2 f) . ((n + 1),(k + 1))) + ((Partial_Sums f) . (n,(k + 1))) =
((((Partial_Sums_in_cod2 f) . ((n + 1),k)) + (f . ((n + 1),(k + 1)))) + ((Partial_Sums f) . (n,k))) + ((Partial_Sums_in_cod1 f) . (n,(k + 1)))
by a6, X1, X2, XXREAL_3:29
.=
((((Partial_Sums_in_cod2 f) . ((n + 1),k)) + ((Partial_Sums f) . (n,k))) + (f . ((n + 1),(k + 1)))) + ((Partial_Sums_in_cod1 f) . (n,(k + 1)))
by X1, XXREAL_3:29
.=
((Partial_Sums f) . ((n + 1),k)) + ((f . ((n + 1),(k + 1))) + ((Partial_Sums_in_cod1 f) . (n,(k + 1))))
by A5, X1, XXREAL_3:29
.=
((Partial_Sums f) . ((n + 1),k)) + ((Partial_Sums_in_cod1 f) . ((n + 1),(k + 1)))
by DefRSM
;
hence
S1[
k + 1]
by DefCSM;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(a3, a4);
hence
(Partial_Sums f) . ((n + 1),m) = ((Partial_Sums_in_cod2 f) . ((n + 1),m)) + ((Partial_Sums f) . (n,m))
; (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m))
defpred S2[ Nat] means (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . ($1,(m + 1)) = ((Partial_Sums_in_cod1 f) . ($1,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . ($1,m));
b1:
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (0,m) = (Partial_Sums_in_cod2 f) . (0,m)
by DefRSM;
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (0,(m + 1)) =
(Partial_Sums_in_cod2 f) . (0,(m + 1))
by DefRSM
.=
((Partial_Sums_in_cod2 f) . (0,m)) + (f . (0,(m + 1)))
by DefCSM
;
then b3:
S2[ 0 ]
by b1, DefRSM;
b4:
for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be
Nat;
( S2[k] implies S2[k + 1] )
assume B5:
S2[
k]
;
S2[k + 1]
b6:
(Partial_Sums_in_cod1 f) . (
(k + 1),
(m + 1))
= ((Partial_Sums_in_cod1 f) . (k,(m + 1))) + (f . ((k + 1),(m + 1)))
by DefRSM;
X3:
(
(Partial_Sums_in_cod1 f) . (
k,
(m + 1))
<> -infty &
f . (
(k + 1),
(m + 1))
<> -infty &
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
k,
m)
<> -infty &
(Partial_Sums_in_cod2 f) . (
(k + 1),
m)
<> -infty &
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
k,
(m + 1))
<> -infty )
by MESFUNC5:def 5;
then X4:
((Partial_Sums_in_cod1 f) . (k,(m + 1))) + (f . ((k + 1),(m + 1))) <> -infty
by XXREAL_3:17;
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
(k + 1),
m)
= ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (k,m)) + ((Partial_Sums_in_cod2 f) . ((k + 1),m))
by DefRSM;
then ((Partial_Sums_in_cod1 f) . ((k + 1),(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . ((k + 1),m)) =
((((Partial_Sums_in_cod1 f) . (k,(m + 1))) + (f . ((k + 1),(m + 1)))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (k,m))) + ((Partial_Sums_in_cod2 f) . ((k + 1),m))
by b6, X3, X4, XXREAL_3:29
.=
((((Partial_Sums_in_cod1 f) . (k,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (k,m))) + (f . ((k + 1),(m + 1)))) + ((Partial_Sums_in_cod2 f) . ((k + 1),m))
by X3, XXREAL_3:29
.=
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (k,(m + 1))) + ((f . ((k + 1),(m + 1))) + ((Partial_Sums_in_cod2 f) . ((k + 1),m)))
by B5, X3, XXREAL_3:29
.=
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (k,(m + 1))) + ((Partial_Sums_in_cod2 f) . ((k + 1),(m + 1)))
by DefCSM
;
hence
S2[
k + 1]
by DefRSM;
verum
end;
for k being Nat holds S2[k]
from NAT_1:sch 2(b3, b4);
hence
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(m + 1)) = ((Partial_Sums_in_cod1 f) . (n,(m + 1))) + ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,m))
; verum