:: deftheorem defines -solution_of_Sierp167 NUMBER18:def 10 :
for s, m being Nat
for f being b₁ -element natural-valued positive-yielding FinSequence holds
( f is m -solution_of_Sierp167 iff Sum ((f ") |^ m) = 1 );