theorem Important167: :: NUMBER18:77

for m, s, k, l, a, b being non zero Nat st ex f being b₂ -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 holds
ex f being (b₂ + (((b₅ |^ b₁) - 1) * b₃)) + (((b₆ |^ b₁) - 1) * b₄) -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167