let k, n be Nat; for f being complex-valued Function st k <= n holds
(f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n))
let f be complex-valued Function; ( k <= n implies (f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n)) )
set k1 = k + 1;
assume A1:
k <= n
; (f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n))
per cases
( k = n or k < n )
by A1, XXREAL_0:1;
suppose A4:
k < n
;
(f,k) +...+ (f,n) = (f . k) + ((f,(k + 1)) +...+ (f,n))then
k + 1
<= n
by NAT_1:13;
then consider h being
complex-valued FinSequence such that A5:
( (
f,
(k + 1))
+...+ (
f,
n)
= Sum h &
len h = (n -' (k + 1)) + 1 )
and A6:
h . (0 + 1) = f . (0 + (k + 1)) & ... &
h . ((n -' (k + 1)) + 1) = f . ((n -' (k + 1)) + (k + 1))
by Th9;
reconsider fk =
f . k as
Complex ;
set h1 =
<*fk*> ^ h;
A7:
(n -' (k + 1)) + 1
= n -' k
by A4, NAT_D:59;
A8:
len <*fk*> = 1
by FINSEQ_1:39;
then
len (<*fk*> ^ h) = (n -' k) + 1
by FINSEQ_1:22, A7, A5;
then A9:
(<*fk*> ^ h) | ((n -' k) + 1) = <*fk*> ^ h
by FINSEQ_1:58;
(<*fk*> ^ h) . (0 + 1) = f . (0 + k) & ... &
(<*fk*> ^ h) . ((n -' k) + 1) = f . ((n -' k) + k)
hence (
f,
k)
+...+ (
f,
n) =
Sum (<*fk*> ^ h)
by Def1, A4, A9
.=
(f . k) + ((f,(k + 1)) +...+ (f,n))
by RVSUM_2:33, A5
;
verum end; end;