let k, m, n be Nat; :: thesis: for f being complex-valued Function st k <= m & m <= n holds
((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,n)) = (f,k) +...+ (f,n)
let f be complex-valued Function; :: thesis: ( k <= m & m <= n implies ((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,n)) = (f,k) +...+ (f,n) )
assume A1: ( k <= m & m <= n ) ; :: thesis: ((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,n)) = (f,k) +...+ (f,n)
defpred S₁[ Nat] means ((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,(m + $1))) = (f,k) +...+ (f,(m + $1));
A2: S₁[ 0 ]

proof

m + 1 > m + 0 by NAT_1:13;
then (f,(m + 1)) +...+ (f,(m + 0)) = 0 by Def1;
hence S₁[ 0 ] ; :: thesis: verum

end;

A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
A5: m + 1 <= (m + 1) + i by NAT_1:11;
m <= m + (i + 1) by NAT_1:11;
hence (f,k) +...+ (f,(m + (i + 1))) = ((f,k) +...+ (f,(m + i))) + (f . ((m + i) + 1)) by A1, XXREAL_0:2, Th12
.= ((f,k) +...+ (f,m)) + (((f,(m + 1)) +...+ (f,(m + i))) + (f . ((m + i) + 1))) by A4
.= ((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,(m + (i + 1)))) by Th12, A5 ;
:: thesis: verum

end;

A6: for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
reconsider nm = n - m as Nat by A1, NAT_1:21;
S₁[nm] by A6;
hence ((f,k) +...+ (f,m)) + ((f,(m + 1)) +...+ (f,n)) = (f,k) +...+ (f,n) ; :: thesis: verum