:: deftheorem defines +... FLEXARY1:def 3 :
for n being Nat
for h being complex-valued FinSequence holds (h,n) +... = (h,n) +...+ (h,(len h));