let n be Nat; :: thesis: for f being finite complex-valued Function holds (f . n) + ((f,(n + 1)) +...) = (f,n) +...
let f be finite complex-valued Function; :: thesis: (f . n) + ((f,(n + 1)) +...) = (f,n) +...
{n} c= NAT by ORDINAL1:def 12;
then reconsider D = ((dom f) /\ NAT) \/ {n} as non empty finite Subset of NAT by XBOOLE_1:8;
reconsider m = max D as Nat by TARSKI:1;
A1: 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 A2: i in dom f ; :: thesis: i <= m
i in NAT by ORDINAL1:def 12;
then i in (dom f) /\ NAT by A2, XBOOLE_0:def 4;
then i in D by XBOOLE_0:def 3;
hence i <= m by XXREAL_2:def 8; :: thesis: verum

end;

then A3: (f,(n + 1)) +... = (f,(n + 1)) +...+ (f,m) by Def2;
A4: (f,n) +... = (f,n) +...+ (f,m) by Def2, A1;
n in {n} by TARSKI:def 1;
then n in D by XBOOLE_0:def 3;
then n <= m by XXREAL_2:def 8;
hence (f . n) + ((f,(n + 1)) +...) = (f,n) +... by Th13, A3, A4; :: thesis: verum