theorem :: NUMBER18:78

for m being non zero Nat ex N being Nat st
for n being non zero Nat st n > N holds
ex f being b₃ -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167