let F be FinSequence of ExtREAL ; for f being FinSequence of REAL st F = f holds
Sum F = Sum f
let f be FinSequence of REAL ; ( F = f implies Sum F = Sum f )
defpred S1[ Nat] means for G being FinSequence of ExtREAL
for g being FinSequence of REAL st G = F | (Seg $1) & g = f | (Seg $1) & $1 <= len F holds
Sum G = Sum g;
F | (Seg (len F)) = F | (len F)
by FINSEQ_1:def 15;
then A1:
F | (Seg (len F)) = F
by FINSEQ_1:58;
assume A2:
F = f
; Sum F = Sum f
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
for
G being
FinSequence of
ExtREAL for
g being
FinSequence of
REAL st
G = F | (Seg (k + 1)) &
g = f | (Seg (k + 1)) &
k + 1
<= len F holds
Sum G = Sum g
proof
let G be
FinSequence of
ExtREAL ;
for g being FinSequence of REAL st G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F holds
Sum G = Sum glet g be
FinSequence of
REAL ;
( G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F implies Sum G = Sum g )
assume that A5:
G = F | (Seg (k + 1))
and A6:
g = f | (Seg (k + 1))
and A7:
k + 1
<= len F
;
Sum G = Sum g
reconsider gk =
g . (k + 1) as
Element of
REAL by XREAL_0:def 1;
reconsider g2 =
<*gk*> as
FinSequence of
REAL ;
reconsider G1 =
G | (Seg k) as
FinSequence of
ExtREAL by FINSEQ_1:18;
reconsider g1 =
g | (Seg k) as
FinSequence of
REAL by FINSEQ_1:18;
len g = k + 1
by A2, A6, A7, FINSEQ_1:17;
then
g = g1 ^ <*(g . (k + 1))*>
by FINSEQ_3:55;
then A10:
Sum g = (Sum g1) + (g . (k + 1))
by RVSUM_1:74;
A11:
k <= k + 1
by NAT_1:11;
len G = k + 1
by A5, A7, FINSEQ_1:17;
then
G = G1 ^ <*(G . (k + 1))*>
by FINSEQ_3:55;
then A12:
Sum G =
(Sum G1) + (Sum <*(G . (k + 1))*>)
by A8, EXTREAL1:10
.=
(Sum G1) + (G . (k + 1))
by EXTREAL1:8
;
k <= k + 1
by NAT_1:11;
then
Seg k c= Seg (k + 1)
by FINSEQ_1:5;
then
(
G1 = F | (Seg k) &
g1 = f | (Seg k) )
by A5, A6, FUNCT_1:51;
then
Sum G1 = Sum g1
by A4, A7, A11, XXREAL_0:2;
hence
Sum G = Sum g
by A2, A5, A6, A12, A10, SUPINF_2:1;
verum
end;
hence
S1[
k + 1]
;
verum
end;
A13:
S1[ 0 ]
by EXTREAL1:7, RVSUM_1:72;
for k being Nat holds S1[k]
from NAT_1:sch 2(A13, A3);
hence
Sum F = Sum f
by A2, A1; verum