let c be complex number ; :: thesis: ( c = (h,n) +... iff c = (h,n) +...+ (h,(len h)) )
A1: (dom h) /\ NAT = dom h by XBOOLE_1:28;
thus ( c = (h,n) +... implies c = (h,n) +...+ (h,(len h)) ) :: thesis: ( c = (h,n) +...+ (h,(len h)) implies c = (h,n) +... )

proof

for i being Nat st i in dom h holds
i <= len h by FINSEQ_3:25;
hence ( c = (h,n) +... implies c = (h,n) +...+ (h,(len h)) ) by Def2, A1; :: thesis: verum

end;

assume A2: c = (h,n) +...+ (h,(len h)) ; :: thesis: c = (h,n) +...
for k being Nat st ( for i being Nat st i in dom h holds
i <= k ) holds
c = (h,n) +...+ (h,k)

proof

let k be Nat; :: thesis: ( ( for i being Nat st i in dom h holds
i <= k ) implies c = (h,n) +...+ (h,k) )
assume A3: for i being Nat st i in dom h holds
i <= k ; :: thesis: c = (h,n) +...+ (h,k)

now :: thesis: len h <= k

per cases ( len h = 0 or len h >= 1 ) by NAT_1:14;

suppose len h = 0 ; :: thesis: len h <= k

hence len h <= k ; :: thesis: verum

end;

suppose len h >= 1 ; :: thesis: len h <= k

then len h in dom h by FINSEQ_3:25;
hence len h <= k by A3; :: thesis: verum

end;

end;

end;

hence c = (h,n) +...+ (h,k) by Th16, A2; :: thesis: verum

end;

hence c = (h,n) +... by A1, Def2; :: thesis: verum