let C1, C2 be complex number ; :: thesis: ( ( for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
C1 = (f,n) +...+ (f,k) ) & ( for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
C2 = (f,n) +...+ (f,k) ) implies C1 = C2 )
assume that
A12: for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
C1 = (f,n) +...+ (f,k) and
A13: for k being Nat st ( for i being Nat st i in dom f holds
i <= k ) holds
C2 = (f,n) +...+ (f,k) ; :: thesis: C1 = C2

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

suppose not (dom f) /\ NAT is empty ; :: thesis: C1 = C2

then reconsider F = (dom f) /\ NAT as non empty finite Subset of NAT by A1;
reconsider m = max F as Nat by TARSKI:1;
A14: for i being Nat st i in dom f holds
i <= m

proof

let i be Nat; :: thesis: ( i in dom f implies i <= m )
assume A15: i in dom f ; :: thesis: i <= m
i in NAT by ORDINAL1:def 12;
then i in F by A15, XBOOLE_0:def 4;
hence i <= m by XXREAL_2:def 8; :: thesis: verum

end;

hence C1 = (f,n) +...+ (f,m) by A12
.= C2 by A14, A13 ;
:: thesis: verum

end;

suppose A16: (dom f) /\ NAT is empty ; :: thesis: C1 = C2

A17: for i being Nat st i in dom f holds
i <= 1

proof

let i be Nat; :: thesis: ( i in dom f implies i <= 1 )
assume A18: i in dom f ; :: thesis: i <= 1
i in NAT by ORDINAL1:def 12;
hence i <= 1 by A18, XBOOLE_0:def 4, A16; :: thesis: verum

end;

hence C1 = (f,n) +...+ (f,1) by A12
.= C2 by A17, A13 ;
:: thesis: verum

end;

end;