let f be Real_Sequence; for n being Nat st f . 0 = 0 holds
Sum (FinSeq (f,n)) = Sum (f |_ (Seg n))
let n be Nat; ( f . 0 = 0 implies Sum (FinSeq (f,n)) = Sum (f |_ (Seg n)) )
assume A0:
f . 0 = 0
; Sum (FinSeq (f,n)) = Sum (f |_ (Seg n))
set f1 = f |_ (Seg n);
set g = FinSeq (f,n);
reconsider f0 = f . 0 as Element of REAL ;
set h = <*f0*> ^ (FinSeq (f,n));
A1:
dom f = NAT
by FUNCT_2:def 1;
A2:
dom (FinSeq (f,n)) = Seg n
by A1, RELAT_1:62;
then
Seg (len (FinSeq (f,n))) = Seg n
by FINSEQ_1:def 3;
then A3:
len (FinSeq (f,n)) = n
by FINSEQ_1:6;
len (<*f0*> ^ (FinSeq (f,n))) = (len <*f0*>) + (len (FinSeq (f,n)))
by FINSEQ_1:22;
then A4:
len (<*f0*> ^ (FinSeq (f,n))) = n + 1
by A3, FINSEQ_1:39;
reconsider g = FinSeq (f,n) as FinSequence of REAL ;
A5:
len <*f0*> = 1
by FINSEQ_1:39;
A6:
for k being Nat st k < n + 1 holds
(f |_ (Seg n)) . k = (<*f0*> ^ (FinSeq (f,n))) . (k + 1)
proof
let k be
Nat;
( k < n + 1 implies (f |_ (Seg n)) . k = (<*f0*> ^ (FinSeq (f,n))) . (k + 1) )
assume
k < n + 1
;
(f |_ (Seg n)) . k = (<*f0*> ^ (FinSeq (f,n))) . (k + 1)
then A7:
k <= n
by NAT_1:13;
per cases
( 1 <= k or k = 0 )
by NAT_1:14;
suppose A8:
1
<= k
;
(f |_ (Seg n)) . k = (<*f0*> ^ (FinSeq (f,n))) . (k + 1)then A9:
k in dom g
by FINSEQ_3:25, A7, A3;
A10:
(f | (Seg n)) . k = f . k
by FUNCT_1:49, A2, FINSEQ_3:25, A7, A3, A8;
(f |_ (Seg n)) . k = f . k
by A2, A8, Th17, FINSEQ_3:25, A7, A3;
hence
(f |_ (Seg n)) . k = (<*f0*> ^ (FinSeq (f,n))) . (k + 1)
by FINSEQ_1:def 7, A5, A9, A10;
verum end; end;
end;
for k being Nat st k >= n + 1 holds
(f |_ (Seg n)) . k = 0
then
Sum (f |_ (Seg n)) = Sum (<*f0*> ^ (FinSeq (f,n)))
by IRRAT_1:18, A6, A4;
then
Sum (f |_ (Seg n)) = f0 + (Sum g)
by RVSUM_1:76;
hence
Sum (FinSeq (f,n)) = Sum (f |_ (Seg n))
by A0; verum