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)

(f |_ (Seg n)) . k = 0

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

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

for k being Nat st k >= n + 1 holds
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;

end;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;

end;

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;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

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;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

(f |_ (Seg n)) . k = 0

proof

then
Sum (f |_ (Seg n)) = Sum (<*f0*> ^ (FinSeq (f,n)))
by IRRAT_1:18, A6, A4;
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;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

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