per cases ( (dom f) /\ NAT = {} or not (dom f) /\ NAT is empty ) ;

suppose A2: (dom f) /\ NAT = {} ; :: thesis: ex b₁ being complex number st
for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
b₁ = (f,n) +...+ (f,k)

take 0 ; :: thesis: for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
0 = (f,n) +...+ (f,k)
let k be Nat; :: thesis: ( ( for i being Nat st i in dom f holds
i <= k ) implies 0 = (f,n) +...+ (f,k) )
assume for i being Nat st i in dom f holds
i <= k ; :: thesis: 0 = (f,n) +...+ (f,k)
for i being Nat st n <= i & i <= k holds
not i in dom f

proof

let i be Nat; :: thesis: ( n <= i & i <= k implies not i in dom f )
i in NAT by ORDINAL1:def 12;
hence ( n <= i & i <= k implies not i in dom f ) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

hence 0 = (f,n) +...+ (f,k) by Th10; :: thesis: verum

end;

suppose not (dom f) /\ NAT is empty ; :: thesis: ex b₁ being complex number st
for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
b₁ = (f,n) +...+ (f,k)

then reconsider F = (dom f) /\ NAT as non empty finite Subset of NAT by A1;
reconsider m = max F as Nat by TARSKI:1;
take t = (f,n) +...+ (f,m); :: thesis: for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
t = (f,n) +...+ (f,k)
let k be Nat; :: thesis: ( ( for i being Nat st i in dom f holds
i <= k ) implies t = (f,n) +...+ (f,k) )
assume A3: for i being Nat st i in dom f holds
i <= k ; :: thesis: t = (f,n) +...+ (f,k)
m in F by XXREAL_2:def 8;
then reconsider km = k - m as Nat by A3, NAT_1:21;

per cases ( n > m or n <= m ) ;

suppose A4: n > m ; :: thesis: t = (f,n) +...+ (f,k)

(f,n) +...+ (f,k) = 0

proof

assume (f,n) +...+ (f,k) <> 0 ; :: thesis: contradiction
then consider i being Nat such that
A5: ( n <= i & i <= k & i in dom f ) by Th10;
i in NAT by ORDINAL1:def 12;
then i in F by A5, XBOOLE_0:def 4;
then i <= m by XXREAL_2:def 8;
hence contradiction by A4, XXREAL_0:2, A5; :: thesis: verum

end;

hence t = (f,n) +...+ (f,k) by A4, Def1; :: thesis: verum

end;

suppose A6: n <= m ; :: thesis: t = (f,n) +...+ (f,k)

defpred S₁[ Nat] means t = (f,n) +...+ (f,(m + $1));
A7: S₁[ 0 ] ;
A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A9: S₁[i] ; :: thesis: S₁[i + 1]
A10: m < (m + i) + 1 by NAT_1:11, NAT_1:13;
then A11: (f,n) +...+ (f,((m + i) + 1)) = ((f,n) +...+ (f,(m + i))) + (f . ((m + i) + 1)) by A6, XXREAL_0:2, Th12
.= t + (f . ((m + i) + 1)) by A9 ;
not (m + i) + 1 in dom f

proof

assume (m + i) + 1 in dom f ; :: thesis: contradiction
then (m + i) + 1 in F by XBOOLE_0:def 4;
hence contradiction by XXREAL_2:def 8, A10; :: thesis: verum

end;

then f . ((m + i) + 1) = 0 by FUNCT_1:def 2;
hence S₁[i + 1] by A11; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A7, A8);
then S₁[km] ;
hence t = (f,n) +...+ (f,k) ; :: thesis: verum

end;

end;

end;

end;