:: deftheorem defines with_sum_of_reciprocals_equal_1 NUMBER17:def 6 :
for f being complex-valued FinSequence holds
( f is with_sum_of_reciprocals_equal_1 iff Sum (f ") = 1 );