now :: thesis: ( f = g implies for C1, C2 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
C1 = Sum (h | ((n -' k) + 1)) ) & ( for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
C2 = Sum (h | ((n -' k) + 1)) ) holds
C1 = C2 )

assume f = g ; :: thesis: for C1, C2 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
C1 = Sum (h | ((n -' k) + 1)) ) & ( for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
C2 = Sum (h | ((n -' k) + 1)) ) holds
C1 = C2
let C1, C2 be complex number ; :: thesis: ( ( for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
C1 = Sum (h | ((n -' k) + 1)) ) & ( for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
C2 = Sum (h | ((n -' k) + 1)) ) implies C1 = C2 )
assume that
A15: for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
C1 = Sum (h | ((n -' k) + 1)) and
A16: for h being complex-valued FinSequence st h . (0 + 1) = f . (0 + k) & ... & h . ((n -' k) + 1) = f . ((n -' k) + k) holds
C2 = Sum (h | ((n -' k) + 1)) ; :: thesis: C1 = C2
deffunc H₁( Nat) -> set = f . ((k + $1) - 1);
set nk = (n -' k) + 1;
consider p being FinSequence such that
A17: ( 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
A18: ( x in dom p & p . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A18;
p . x = f . ((k + x) - 1) by A18, A17;
hence y in COMPLEX by A18, XCMPLX_0:def 2; :: thesis: verum

end;

then reconsider p = p as complex-valued FinSequence by VALUED_0:def 1;
p . (0 + 1) = f . (0 + k) & ... & p . ((n -' k) + 1) = f . ((n -' k) + k)

proof

let i be Nat; :: thesis: ( not 0 <= i or not i <= n -' k or p . (i + 1) = f . (i + k) )
assume ( 0 <= i & i <= n -' k ) ; :: thesis: p . (i + 1) = f . (i + k)
then ( 1 <= i + 1 & i + 1 <= (n -' k) + 1 ) by NAT_1:11, XREAL_1:6;
then p . (i + 1) = f . ((k + (i + 1)) - 1) by A17, FINSEQ_3:25;
hence p . (i + 1) = f . (i + k) ; :: thesis: verum

end;

then ( C1 = Sum (p | ((n -' k) + 1)) & C2 = Sum (p | ((n -' k) + 1)) ) by A15, A16;
hence C1 = C2 ; :: thesis: verum

end;

hence for b₁, b₂ being complex number holds
( ( f = g & k <= n & ( 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)) ) & ( 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)) ) implies b₁ = b₂ ) & ( ( not f = g or not k <= n ) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) ) ; :: thesis: verum