let c be complex number ; ( 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)) )
( c = (h,n) +...+ (h,(len h)) implies c = (h,n) +... )
assume A2:
c = (h,n) +...+ (h,(len h))
; 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)
hence
c = (h,n) +...
by A1, Def2; verum