let k, n be Nat; for f being complex-valued Function st k <= n + 1 holds
(f,k) +...+ (f,(n + 1)) = ((f,k) +...+ (f,n)) + (f . (n + 1))
let f be complex-valued Function; ( k <= n + 1 implies (f,k) +...+ (f,(n + 1)) = ((f,k) +...+ (f,n)) + (f . (n + 1)) )
set n1 = n + 1;
assume A1:
k <= n + 1
; (f,k) +...+ (f,(n + 1)) = ((f,k) +...+ (f,n)) + (f . (n + 1))
per cases
( k = n + 1 or k <= n )
by A1, NAT_1:8;
suppose A2:
k = n + 1
;
(f,k) +...+ (f,(n + 1)) = ((f,k) +...+ (f,n)) + (f . (n + 1))then
k > n
by NAT_1:13;
then
( (
f,
k)
+...+ (
f,
n)
= 0 & (
f,
k)
+...+ (
f,
(n + 1))
= f . k )
by A2, Th11, Def1;
hence
(
f,
k)
+...+ (
f,
(n + 1))
= ((f,k) +...+ (f,n)) + (f . (n + 1))
by A2;
verum end; suppose A3:
k <= n
;
(f,k) +...+ (f,(n + 1)) = ((f,k) +...+ (f,n)) + (f . (n + 1))then consider h being
complex-valued FinSequence such that A4:
( (
f,
k)
+...+ (
f,
n)
= Sum h &
len h = (n -' k) + 1 )
and A5:
h . (0 + 1) = f . (0 + k) & ... &
h . ((n -' k) + 1) = f . ((n -' k) + k)
by Th9;
A6:
(n + 1) -' k = (n -' k) + 1
by A3, NAT_D:38;
set fn =
f . (n + 1);
reconsider fn =
f . (n + 1) as
Complex ;
set h1 =
h ^ <*fn*>;
A7:
len (h ^ <*fn*>) = ((n + 1) -' k) + 1
by A6, A4, FINSEQ_2:16;
(h ^ <*fn*>) . (0 + 1) = f . (0 + k) & ... &
(h ^ <*fn*>) . (((n + 1) -' k) + 1) = f . (((n + 1) -' k) + k)
then (
f,
k)
+...+ (
f,
(n + 1)) =
Sum ((h ^ <*fn*>) | (((n + 1) -' k) + 1))
by A1, Def1
.=
Sum (h ^ <*fn*>)
by A7, FINSEQ_1:58
;
hence
(
f,
k)
+...+ (
f,
(n + 1))
= ((f,k) +...+ (f,n)) + (f . (n + 1))
by A4, RVSUM_2:31;
verum end; end;