let f1, f2 be without-infty Function of [:NAT,NAT:],ExtREAL; ( Partial_Sums_in_cod2 (f1 + f2) = (Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2) & Partial_Sums_in_cod1 (f1 + f2) = (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2) )
set CS1 = Partial_Sums_in_cod2 f1;
set CS2 = Partial_Sums_in_cod2 f2;
set CS12 = Partial_Sums_in_cod2 (f1 + f2);
set RS1 = Partial_Sums_in_cod1 f1;
set RS2 = Partial_Sums_in_cod1 f2;
set RS12 = Partial_Sums_in_cod1 (f1 + f2);
now for n, m being Element of NAT holds (Partial_Sums_in_cod2 (f1 + f2)) . (n,m) = ((Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2)) . (n,m)let n,
m be
Element of
NAT ;
(Partial_Sums_in_cod2 (f1 + f2)) . (n,m) = ((Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2)) . (n,m)defpred S1[
Nat]
means (Partial_Sums_in_cod2 (f1 + f2)) . (
n,$1)
= ((Partial_Sums_in_cod2 f1) . (n,$1)) + ((Partial_Sums_in_cod2 f2) . (n,$1));
(Partial_Sums_in_cod2 (f1 + f2)) . (
n,
0) =
(f1 + f2) . (
n,
0)
by DefCSM
.=
(f1 . (n,0)) + (f2 . (n,0))
by Th11
.=
((Partial_Sums_in_cod2 f1) . (n,0)) + (f2 . (n,0))
by DefCSM
;
then a1:
S1[
0 ]
by DefCSM;
a2:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume a3:
S1[
k]
;
S1[k + 1]
X1:
(
(Partial_Sums_in_cod2 f1) . (
n,
k)
<> -infty &
(Partial_Sums_in_cod2 f2) . (
n,
k)
<> -infty &
f1 . (
n,
(k + 1))
<> -infty &
f2 . (
n,
(k + 1))
<> -infty &
(f1 + f2) . (
n,
(k + 1))
<> -infty )
by MESFUNC5:def 5;
then X2:
((Partial_Sums_in_cod2 f2) . (n,k)) + (f2 . (n,(k + 1))) <> -infty
by XXREAL_3:17;
(Partial_Sums_in_cod2 (f1 + f2)) . (
n,
(k + 1)) =
((Partial_Sums_in_cod2 (f1 + f2)) . (n,k)) + ((f1 + f2) . (n,(k + 1)))
by DefCSM
.=
((Partial_Sums_in_cod2 f1) . (n,k)) + (((f1 + f2) . (n,(k + 1))) + ((Partial_Sums_in_cod2 f2) . (n,k)))
by a3, X1, XXREAL_3:29
.=
((Partial_Sums_in_cod2 f1) . (n,k)) + (((f1 . (n,(k + 1))) + (f2 . (n,(k + 1)))) + ((Partial_Sums_in_cod2 f2) . (n,k)))
by Th11
.=
((Partial_Sums_in_cod2 f1) . (n,k)) + ((f1 . (n,(k + 1))) + (((Partial_Sums_in_cod2 f2) . (n,k)) + (f2 . (n,(k + 1)))))
by X1, XXREAL_3:29
.=
(((Partial_Sums_in_cod2 f1) . (n,k)) + (f1 . (n,(k + 1)))) + (((Partial_Sums_in_cod2 f2) . (n,k)) + (f2 . (n,(k + 1))))
by X1, X2, XXREAL_3:29
.=
((Partial_Sums_in_cod2 f1) . (n,(k + 1))) + (((Partial_Sums_in_cod2 f2) . (n,k)) + (f2 . (n,(k + 1))))
by DefCSM
;
hence
S1[
k + 1]
by DefCSM;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(a1, a2);
then
S1[
m]
;
hence
(Partial_Sums_in_cod2 (f1 + f2)) . (
n,
m)
= ((Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2)) . (
n,
m)
by Th11;
verum end;
hence
Partial_Sums_in_cod2 (f1 + f2) = (Partial_Sums_in_cod2 f1) + (Partial_Sums_in_cod2 f2)
by BINOP_1:2; Partial_Sums_in_cod1 (f1 + f2) = (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2)
now for n, m being Element of NAT holds (Partial_Sums_in_cod1 (f1 + f2)) . (n,m) = ((Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2)) . (n,m)let n,
m be
Element of
NAT ;
(Partial_Sums_in_cod1 (f1 + f2)) . (n,m) = ((Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2)) . (n,m)defpred S1[
Nat]
means (Partial_Sums_in_cod1 (f1 + f2)) . ($1,
m)
= ((Partial_Sums_in_cod1 f1) . ($1,m)) + ((Partial_Sums_in_cod1 f2) . ($1,m));
(Partial_Sums_in_cod1 (f1 + f2)) . (
0,
m) =
(f1 + f2) . (
0,
m)
by DefRSM
.=
(f1 . (0,m)) + (f2 . (0,m))
by Th11
.=
((Partial_Sums_in_cod1 f1) . (0,m)) + (f2 . (0,m))
by DefRSM
;
then a4:
S1[
0 ]
by DefRSM;
a5:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume a6:
S1[
k]
;
S1[k + 1]
X3:
(
(Partial_Sums_in_cod1 f1) . (
k,
m)
<> -infty &
(Partial_Sums_in_cod1 f2) . (
k,
m)
<> -infty &
f1 . (
(k + 1),
m)
<> -infty &
f2 . (
(k + 1),
m)
<> -infty &
(f1 + f2) . (
(k + 1),
m)
<> -infty )
by MESFUNC5:def 5;
then X4:
((Partial_Sums_in_cod1 f2) . (k,m)) + (f2 . ((k + 1),m)) <> -infty
by XXREAL_3:17;
(Partial_Sums_in_cod1 (f1 + f2)) . (
(k + 1),
m) =
((Partial_Sums_in_cod1 (f1 + f2)) . (k,m)) + ((f1 + f2) . ((k + 1),m))
by DefRSM
.=
((Partial_Sums_in_cod1 f1) . (k,m)) + (((f1 + f2) . ((k + 1),m)) + ((Partial_Sums_in_cod1 f2) . (k,m)))
by a6, X3, XXREAL_3:29
.=
((Partial_Sums_in_cod1 f1) . (k,m)) + (((f1 . ((k + 1),m)) + (f2 . ((k + 1),m))) + ((Partial_Sums_in_cod1 f2) . (k,m)))
by Th11
.=
((Partial_Sums_in_cod1 f1) . (k,m)) + ((f1 . ((k + 1),m)) + (((Partial_Sums_in_cod1 f2) . (k,m)) + (f2 . ((k + 1),m))))
by X3, XXREAL_3:29
.=
(((Partial_Sums_in_cod1 f1) . (k,m)) + (f1 . ((k + 1),m))) + (((Partial_Sums_in_cod1 f2) . (k,m)) + (f2 . ((k + 1),m)))
by X3, X4, XXREAL_3:29
.=
((Partial_Sums_in_cod1 f1) . ((k + 1),m)) + (((Partial_Sums_in_cod1 f2) . (k,m)) + (f2 . ((k + 1),m)))
by DefRSM
;
hence
S1[
k + 1]
by DefRSM;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(a4, a5);
then
S1[
n]
;
hence
(Partial_Sums_in_cod1 (f1 + f2)) . (
n,
m)
= ((Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2)) . (
n,
m)
by Th11;
verum end;
hence
Partial_Sums_in_cod1 (f1 + f2) = (Partial_Sums_in_cod1 f1) + (Partial_Sums_in_cod1 f2)
by BINOP_1:2; verum