:: deftheorem defines with_sum_of_squares_of_reciprocals_equal_1 NUMBER17:def 16 :
for f being complex-valued FinSequence holds
( f is with_sum_of_squares_of_reciprocals_equal_1 iff Sum ((f ") ^2) = 1 );