let F, G, H be FinSequence of ExtREAL ; ( not -infty in rng F & not -infty in rng G & dom F = dom G & H = F + G implies Sum H = (Sum F) + (Sum G) )
assume that
A1:
( not -infty in rng F & not -infty in rng G )
and
A3:
dom F = dom G
and
A4:
H = F + G
; Sum H = (Sum F) + (Sum G)
B1:
for y being object st y in rng F holds
not y in {-infty}
by A1, TARSKI:def 1;
then A7:
F " {-infty} = {}
by XBOOLE_0:3, RELAT_1:138;
B2:
for y being object st y in rng G holds
not y in {-infty}
by A1, TARSKI:def 1;
then A10:
G " {-infty} = {}
by XBOOLE_0:3, RELAT_1:138;
A11: dom H =
((dom F) /\ (dom G)) \ (((F " {-infty}) /\ (G " {+infty})) \/ ((F " {+infty}) /\ (G " {-infty})))
by A4, MESFUNC1:def 3
.=
dom F
by A3, A7, A10
;
then A12:
len H = len F
by FINSEQ_3:29;
consider h being Function of NAT,ExtREAL such that
A13:
( Sum H = h . (len H) & h . 0 = 0. & ( for i being Nat st i < len H holds
h . (i + 1) = (h . i) + (H . (i + 1)) ) )
by EXTREAL1:def 2;
consider f being Function of NAT,ExtREAL such that
A16:
( Sum F = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) )
by EXTREAL1:def 2;
consider g being Function of NAT,ExtREAL such that
A19:
( Sum G = g . (len G) & g . 0 = 0. & ( for i being Nat st i < len G holds
g . (i + 1) = (g . i) + (G . (i + 1)) ) )
by EXTREAL1:def 2;
defpred S1[ Nat] means ( $1 <= len H implies h . $1 = (f . $1) + (g . $1) );
A22:
len H = len G
by A3, A11, FINSEQ_3:29;
A23:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A24:
S1[
k]
;
S1[k + 1]
assume A25:
k + 1
<= len H
;
h . (k + 1) = (f . (k + 1)) + (g . (k + 1))
A26:
k < len H
by A25, NAT_1:13;
A27:
(
f . (k + 1) = (f . k) + (F . (k + 1)) &
g . (k + 1) = (g . k) + (G . (k + 1)) )
by A16, A19, A12, A22, A25, NAT_1:13;
A28:
k + 1
in dom H
by A25, NAT_1:11, FINSEQ_3:25;
A29:
(
f . k <> -infty &
g . k <> -infty &
F . (k + 1) <> -infty &
G . (k + 1) <> -infty )
proof
defpred S2[
Nat]
means ( $1
<= len H implies
g . $1
<> -infty );
defpred S3[
Nat]
means ( $1
<= len H implies
f . $1
<> -infty );
A30:
for
m being
Nat st
S3[
m] holds
S3[
m + 1]
proof
let m be
Nat;
( S3[m] implies S3[m + 1] )
assume A31:
S3[
m]
;
S3[m + 1]
assume A32:
m + 1
<= len H
;
f . (m + 1) <> -infty
then
m + 1
in dom H
by NAT_1:11, FINSEQ_3:25;
then
not
F . (m + 1) in {-infty}
by B1, A11, FUNCT_1:3;
then A33:
F . (m + 1) <> -infty
by TARSKI:def 1;
f . (m + 1) = (f . m) + (F . (m + 1))
by A12, A16, A32, NAT_1:13;
hence
f . (m + 1) <> -infty
by A33, A32, NAT_1:13, A31, XXREAL_3:17;
verum
end;
A34:
S3[
0 ]
by A16;
for
i being
Nat holds
S3[
i]
from NAT_1:sch 2(A34, A30);
hence
f . k <> -infty
by A26;
( g . k <> -infty & F . (k + 1) <> -infty & G . (k + 1) <> -infty )
A35:
for
m being
Nat st
S2[
m] holds
S2[
m + 1]
proof
let m be
Nat;
( S2[m] implies S2[m + 1] )
assume A36:
S2[
m]
;
S2[m + 1]
assume A37:
m + 1
<= len H
;
g . (m + 1) <> -infty
then
m + 1
in dom H
by NAT_1:11, FINSEQ_3:25;
then
not
G . (m + 1) in {-infty}
by B2, A11, A3, FUNCT_1:3;
then A38:
G . (m + 1) <> -infty
by TARSKI:def 1;
g . (m + 1) = (g . m) + (G . (m + 1))
by A19, A22, A37, NAT_1:13;
hence
g . (m + 1) <> -infty
by A38, A37, NAT_1:13, A36, XXREAL_3:17;
verum
end;
A39:
S2[
0 ]
by A19;
for
i being
Nat holds
S2[
i]
from NAT_1:sch 2(A39, A35);
hence
g . k <> -infty
by A26;
( F . (k + 1) <> -infty & G . (k + 1) <> -infty )
thus
F . (k + 1) <> -infty
by A1, A11, A28, FUNCT_1:3;
G . (k + 1) <> -infty
thus
G . (k + 1) <> -infty
by A1, A3, A11, A28, FUNCT_1:3;
verum
end;
then A40:
(f . k) + (F . (k + 1)) <> -infty
by XXREAL_3:17;
A41:
h . (k + 1) =
((f . k) + (g . k)) + (H . (k + 1))
by A13, A24, A25, NAT_1:13
.=
((f . k) + (g . k)) + ((F . (k + 1)) + (G . (k + 1)))
by A4, A28, MESFUNC1:def 3
;
(f . k) + (g . k) <> -infty
by A29, XXREAL_3:17;
then h . (k + 1) =
(((f . k) + (g . k)) + (F . (k + 1))) + (G . (k + 1))
by A41, A29, XXREAL_3:29
.=
(((f . k) + (F . (k + 1))) + (g . k)) + (G . (k + 1))
by A29, XXREAL_3:29
.=
(f . (k + 1)) + (g . (k + 1))
by A27, A29, A40, XXREAL_3:29
;
hence
h . (k + 1) = (f . (k + 1)) + (g . (k + 1))
;
verum
end;
A42:
S1[ 0 ]
by A16, A19, A13;
for i being Nat holds S1[i]
from NAT_1:sch 2(A42, A23);
hence
Sum H = (Sum F) + (Sum G)
by A16, A19, A13, A12, A22; verum