:: deftheorem defines a_solution_of_Sierp168 NUMBER15:def 12 :
for s being Nat
for f being b1 + 1 -element complex-valued FinSequence holds
( f is a_solution_of_Sierp168 iff Sum (((f | s) ") ^2) = 1 / ((f . (s + 1)) ^2) );