let f be without-infty Function of [:NAT,NAT:],ExtREAL; for m, n being Nat holds (Partial_Sums f) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,n)
let m, n be Nat; (Partial_Sums f) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,n)
defpred S1[ Nat] means for m being Nat holds (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,$1) = (Partial_Sums f) . (m,$1);
defpred S2[ Nat] means (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . ($1,0) = (Partial_Sums f) . ($1,0);
Y3: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (0,0) =
(Partial_Sums_in_cod2 f) . (0,0)
by DefRSM
.=
f . (0,0)
by DefCSM
;
(Partial_Sums f) . (0,0) =
(Partial_Sums_in_cod1 f) . (0,0)
by DefCSM
.=
f . (0,0)
by DefRSM
;
then Y1:
S2[ 0 ]
by Y3;
Y2:
for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be
Nat;
( S2[i] implies S2[i + 1] )
assume Y3:
S2[
i]
;
S2[i + 1]
Y4:
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
(i + 1),
0) =
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (i,0)) + ((Partial_Sums_in_cod2 f) . ((i + 1),0))
by DefRSM
.=
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (i,0)) + (f . ((i + 1),0))
by DefCSM
;
(Partial_Sums f) . (
(i + 1),
0) =
(Partial_Sums_in_cod1 f) . (
(i + 1),
0)
by DefCSM
.=
((Partial_Sums_in_cod1 f) . (i,0)) + (f . ((i + 1),0))
by DefRSM
.=
((Partial_Sums f) . (i,0)) + (f . ((i + 1),0))
by DefCSM
;
hence
S2[
i + 1]
by Y3, Y4;
verum
end;
for n being Nat holds S2[n]
from NAT_1:sch 2(Y1, Y2);
then X1:
S1[ 0 ]
;
X2:
for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume Z3:
S1[
j]
;
S1[j + 1]
for
m being
Nat holds
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
m,
(j + 1))
= (Partial_Sums f) . (
m,
(j + 1))
proof
let n be
Nat;
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (n,(j + 1)) = (Partial_Sums f) . (n,(j + 1))
defpred S3[
Nat]
means (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . ($1,
(j + 1))
= (Partial_Sums f) . ($1,
(j + 1));
Z4:
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
0,
(j + 1)) =
(Partial_Sums_in_cod2 f) . (
0,
(j + 1))
by DefRSM
.=
((Partial_Sums_in_cod2 f) . (0,j)) + (f . (0,(j + 1)))
by DefCSM
.=
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (0,j)) + (f . (0,(j + 1)))
by DefRSM
;
(Partial_Sums f) . (
0,
(j + 1)) =
((Partial_Sums f) . (0,j)) + ((Partial_Sums_in_cod1 f) . (0,(j + 1)))
by DefCSM
.=
((Partial_Sums f) . (0,j)) + (f . (0,(j + 1)))
by DefRSM
.=
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (0,j)) + (f . (0,(j + 1)))
by Z3
;
then Z1:
S3[
0 ]
by Z4;
Z2:
for
i being
Nat st
S3[
i] holds
S3[
i + 1]
proof
let i be
Nat;
( S3[i] implies S3[i + 1] )
assume
S3[
i]
;
S3[i + 1]
W1:
(
(Partial_Sums f) . (
i,
j)
<> -infty &
(Partial_Sums_in_cod1 f) . (
i,
(j + 1))
<> -infty &
(Partial_Sums_in_cod2 f) . (
(i + 1),
j)
<> -infty &
f . (
(i + 1),
(j + 1))
<> -infty &
(Partial_Sums_in_cod1 f) . (
(i + 1),
(j + 1))
<> -infty &
(Partial_Sums_in_cod2 f) . (
(i + 1),
j)
<> -infty )
by MESFUNC5:def 5;
then W2:
((Partial_Sums f) . (i,j)) + ((Partial_Sums_in_cod1 f) . (i,(j + 1))) <> -infty
by XXREAL_3:17;
Z6:
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
i,
j)
= (Partial_Sums f) . (
i,
j)
by Z3;
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
(i + 1),
(j + 1)) =
((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (i,(j + 1))) + ((Partial_Sums_in_cod2 f) . ((i + 1),(j + 1)))
by DefRSM
.=
(((Partial_Sums f) . (i,j)) + ((Partial_Sums_in_cod1 f) . (i,(j + 1)))) + ((Partial_Sums_in_cod2 f) . ((i + 1),(j + 1)))
by Z6, Th47
.=
(((Partial_Sums f) . (i,j)) + ((Partial_Sums_in_cod1 f) . (i,(j + 1)))) + (((Partial_Sums_in_cod2 f) . ((i + 1),j)) + (f . ((i + 1),(j + 1))))
by DefCSM
.=
((((Partial_Sums f) . (i,j)) + ((Partial_Sums_in_cod1 f) . (i,(j + 1)))) + (f . ((i + 1),(j + 1)))) + ((Partial_Sums_in_cod2 f) . ((i + 1),j))
by W1, W2, XXREAL_3:29
.=
(((Partial_Sums f) . (i,j)) + (((Partial_Sums_in_cod1 f) . (i,(j + 1))) + (f . ((i + 1),(j + 1))))) + ((Partial_Sums_in_cod2 f) . ((i + 1),j))
by W1, XXREAL_3:29
.=
(((Partial_Sums f) . (i,j)) + ((Partial_Sums_in_cod1 f) . ((i + 1),(j + 1)))) + ((Partial_Sums_in_cod2 f) . ((i + 1),j))
by DefRSM
.=
(((Partial_Sums f) . (i,j)) + ((Partial_Sums_in_cod2 f) . ((i + 1),j))) + ((Partial_Sums_in_cod1 f) . ((i + 1),(j + 1)))
by W1, XXREAL_3:29
.=
((Partial_Sums f) . ((i + 1),j)) + ((Partial_Sums_in_cod1 f) . ((i + 1),(j + 1)))
by Th47
;
hence
S3[
i + 1]
by DefCSM;
verum
end;
for
n being
Nat holds
S3[
n]
from NAT_1:sch 2(Z1, Z2);
hence
(Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (
n,
(j + 1))
= (Partial_Sums f) . (
n,
(j + 1))
;
verum
end;
hence
S1[
j + 1]
;
verum
end;
for m being Nat holds S1[m]
from NAT_1:sch 2(X1, X2);
hence
(Partial_Sums f) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,n)
; verum