let X be non empty set ; for F being without_+infty-valued FinSequence of Funcs (X,ExtREAL) holds Partial_Sums F is without_+infty-valued
let F be without_+infty-valued FinSequence of Funcs (X,ExtREAL); Partial_Sums F is without_+infty-valued
defpred S1[ Nat] means ( $1 in dom (Partial_Sums F) implies (Partial_Sums F) . $1 is without+infty );
A1:
S1[ 0 ]
by FINSEQ_3:24;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
B1:
len F = len (Partial_Sums F)
by DEF13;
then A4:
dom F = dom (Partial_Sums F)
by FINSEQ_3:29;
assume A5:
n + 1
in dom (Partial_Sums F)
;
(Partial_Sums F) . (n + 1) is without+infty
per cases
( n = 0 or n <> 0 )
;
suppose A7:
n <> 0
;
(Partial_Sums F) . (n + 1) is without+infty then A8:
n >= 1
by NAT_1:14;
n + 1
<= len F
by A5, B1, FINSEQ_3:25;
then A9:
n < len F
by NAT_1:13;
F . (n + 1) is
without+infty
by A4, A5, DEF10;
then reconsider p =
(Partial_Sums F) /. n,
q =
F /. (n + 1) as
V176()
Function of
X,
ExtREAL by A3, A4, A5, A8, A9, FINSEQ_3:25, PARTFUN1:def 6;
p + q is
V176()
Function of
X,
ExtREAL
;
hence
(Partial_Sums F) . (n + 1) is
without+infty
by A7, A9, DEF13, NAT_1:14;
verum end; end;
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
Partial_Sums F is without_+infty-valued
; verum