let k, n be Nat; :: thesis: for h being complex-valued FinSequence st n >= len h holds
(h,k) +...+ (h,n) = (h,k) +...+ (h,(len h))
let h be complex-valued FinSequence; :: thesis: ( n >= len h implies (h,k) +...+ (h,n) = (h,k) +...+ (h,(len h)) )
assume A1: n >= len h ; :: thesis: (h,k) +...+ (h,n) = (h,k) +...+ (h,(len h))

per cases ( k > len h or k <= len h ) ;

suppose k > len h ; :: thesis: (h,k) +...+ (h,n) = (h,k) +...+ (h,(len h))

then ( (h,k) +...+ (h,(len h)) = 0 & (h,k) +...+ (h,n) = 0 ) by Th15;
hence (h,k) +...+ (h,n) = (h,k) +...+ (h,(len h)) ; :: thesis: verum

end;

suppose A2: k <= len h ; :: thesis: (h,k) +...+ (h,n) = (h,k) +...+ (h,(len h))

defpred S₁[ Nat] means (h,k) +...+ (h,((len h) + $1)) = (h,k) +...+ (h,(len h));
A3: S₁[ 0 ] ;
A4: 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 A5: S₁[i] ; :: thesis: S₁[i + 1]
(len h) + (i + 1) > (len h) + 0 by XREAL_1:6;
then A6: not (len h) + (i + 1) in dom h by FINSEQ_3:25;
A7: len h <= (len h) + (i + 1) by NAT_1:11;
A8: h . ((len h) + (i + 1)) = 0 by A6, FUNCT_1:def 2;
(h,k) +...+ (h,(((len h) + i) + 1)) = ((h,k) +...+ (h,((len h) + i))) + (h . (((len h) + i) + 1)) by Th12, A7, XXREAL_0:2, A2;
hence S₁[i + 1] by A8, A5; :: thesis: verum

end;

A9: for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
reconsider nl = n - (len h) as Nat by A1, NAT_1:21;
S₁[nl] by A9;
hence (h,k) +...+ (h,n) = (h,k) +...+ (h,(len h)) ; :: thesis: verum

end;

end;