let f be Real_Sequence; :: thesis: for n being Nat st f . 0 = 0 holds
Sum (FinSeq (f,n)) = Sum (f |_ (Seg n))
let n be Nat; :: thesis: ( f . 0 = 0 implies Sum (FinSeq (f,n)) = Sum (f |_ (Seg n)) )
assume A0: f . 0 = 0 ; :: thesis: 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; :: thesis: ( k < n + 1 implies (f |_ (Seg n)) . k = (<*f0*> ^ (FinSeq (f,n))) . (k + 1) )
assume k < n + 1 ; :: thesis: (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 ; :: thesis: (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; :: thesis: verum
end;
suppose A11: k = 0 ; :: thesis: (f |_ (Seg n)) . k = (<*f0*> ^ (FinSeq (f,n))) . (k + 1)
then not k in Seg n by FINSEQ_1:1;
then not k in dom (f | (Seg n)) by RELAT_1:57;
then (f |_ (Seg n)) . k = (NAT --> 0) . k by FUNCT_4:11;
hence (f |_ (Seg n)) . k = (<*f0*> ^ (FinSeq (f,n))) . (k + 1) by A0, A11; :: thesis: verum
end;
end;
end;
for k being Nat st k >= n + 1 holds
(f |_ (Seg n)) . k = 0
proof
let k be Nat; :: thesis: ( k >= n + 1 implies (f |_ (Seg n)) . k = 0 )
assume k >= n + 1 ; :: thesis: (f |_ (Seg n)) . k = 0
then k > n by XXREAL_0:2, NAT_1:16;
then not k in Seg n by FINSEQ_1:1;
then not k in dom (f | (Seg n)) by RELAT_1:57;
then (f |_ (Seg n)) . k = (NAT --> 0) . k by FUNCT_4:11
.= 0 ;
hence (f |_ (Seg n)) . k = 0 ; :: thesis: verum
end;
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; :: thesis: verum