per cases ( f <> g or n < k or ( f = g & n >= k ) ) ;

suppose ( f <> g or n < k ) ; :: thesis: ( ( f = g & k <= n implies ex b₁ being complex number st
for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b₁ = Sum (h | ((n -' k) + 1)) ) & ( ( not f = g or not k <= n ) implies ex b₁ being complex number st b₁ = 0 ) )

hence ( ( f = g & k <= n implies ex b₁ being complex number st
for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b₁ = Sum (h | ((n -' k) + 1)) ) & ( ( not f = g or not k <= n ) implies ex b₁ being complex number st b₁ = 0 ) ) ; :: thesis: verum

end;

suppose ( f = g & n >= k ) ; :: thesis: ( ( f = g & k <= n implies ex b₁ being complex number st
for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b₁ = Sum (h | ((n -' k) + 1)) ) & ( ( not f = g or not k <= n ) implies ex b₁ being complex number st b₁ = 0 ) )

deffunc H₁( Nat) -> set = f . ((k + $1) - 1);
set kn = (n -' k) + 1;
consider p being FinSequence such that
A1: ( len p = (n -' k) + 1 & ( for i being Nat st i in dom p holds
p . i = H₁(i) ) ) from FINSEQ_1:sch 2();
rng p c= COMPLEX

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in COMPLEX )
assume y in rng p ; :: thesis: y in COMPLEX
then consider x being object such that
A2: ( x in dom p & p . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A2;
p . x = f . ((k + x) - 1) by A2, A1;
hence y in COMPLEX by A2, XCMPLX_0:def 2; :: thesis: verum

end;

then reconsider p = p as complex-valued FinSequence by VALUED_0:def 1;
reconsider S = Sum p as complex number by TARSKI:1;
A3: Sum (p | ((n -' k) + 1)) = S by A1, FINSEQ_1:58;
for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
Sum (p | ((n -' k) + 1)) = Sum (h | ((n -' k) + 1))

proof

let h be complex-valued FinSequence; :: thesis: ( h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) implies Sum (p | ((n -' k) + 1)) = Sum (h | ((n -' k) + 1)) )
assume A4: h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) ; :: thesis: Sum (p | ((n -' k) + 1)) = Sum (h | ((n -' k) + 1))
defpred S₁[ Nat] means ( $1 <= (n -' k) + 1 implies Sum (h | $1) = Sum (p | $1) );
A5: S₁[ 0 ] ;
A6: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
set i1 = i + 1;
assume A7: S₁[i] ; :: thesis: S₁[i + 1]
assume A8: i + 1 <= (n -' k) + 1 ; :: thesis: Sum (h | (i + 1)) = Sum (p | (i + 1))
A9: 1 <= i + 1 by NAT_1:11;
then p | (i + 1) = (p | i) ^ <*(p . (i + 1))*> by FINSEQ_5:10, A1, A8, FINSEQ_3:25;
then A10: Sum (p | (i + 1)) = (Sum (p | i)) + (p . (i + 1)) by RVSUM_2:31;
A11: p . (i + 1) = f . ((k + (i + 1)) - 1) by A1, A9, A8, FINSEQ_3:25;
i <= n -' k by A8, XREAL_1:6;
then A12: f . (k + i) = h . (1 + i) by A4;

per cases ( i + 1 <= len h or i + 1 > len h ) ;

suppose i + 1 <= len h ; :: thesis: Sum (h | (i + 1)) = Sum (p | (i + 1))

then i + 1 in dom h by NAT_1:11, FINSEQ_3:25;
then h | (i + 1) = (h | i) ^ <*(h . (i + 1))*> by FINSEQ_5:10;
hence Sum (h | (i + 1)) = Sum (p | (i + 1)) by RVSUM_2:31, A8, NAT_1:13, A7, A10, A11, A12; :: thesis: verum

end;

suppose A13: i + 1 > len h ; :: thesis: Sum (h | (i + 1)) = Sum (p | (i + 1))

then not i + 1 in dom h by FINSEQ_3:25;
then A14: h . (i + 1) = 0 by FUNCT_1:def 2;
h | i = h by A13, NAT_1:13, FINSEQ_1:58;
hence Sum (h | (i + 1)) = Sum (p | (i + 1)) by A8, NAT_1:13, A7, A10, A11, A12, A13, FINSEQ_1:58, A14; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A5, A6);
hence Sum (p | ((n -' k) + 1)) = Sum (h | ((n -' k) + 1)) ; :: thesis: verum

end;

hence ( ( f = g & k <= n implies ex b₁ being complex number st
for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
b₁ = Sum (h | ((n -' k) + 1)) ) & ( ( not f = g or not k <= n ) implies ex b₁ being complex number st b₁ = 0 ) ) by A3; :: thesis: verum

end;

end;