let m be non zero Nat; ex N being Nat st
for n being non zero Nat st n > N holds
ex f being b2 -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167
reconsider s = 2 |^ m as non zero Nat ;
set f = s |-> 2;
len (s |-> 2) = s
;
then reconsider f = s |-> 2 as s -element natural-valued positive-yielding FinSequence by CARD_1:def 7;
A1:
f is m -solution_of_Sierp167
by Expand0;
reconsider a = 2 as non zero Nat ;
reconsider b = (2 |^ m) - 1 as non zero Nat ;
take N = (((2 |^ m) - 1) * ((((2 |^ m) - 1) |^ m) - 1)) + s; for n being non zero Nat st n > N holds
ex f being b1 -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167
let n be non zero Nat; ( n > N implies ex f being n -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 )
assume
n > N
; ex f being n -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167
then k1:
n - s > ((((2 |^ m) - 1) * ((((2 |^ m) - 1) |^ m) - 1)) + s) - s
by XREAL_1:8;
consider k, l being non zero Nat such that
A2:
n - s = (((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l)
by k1, Lemma167A;
A4:
n = ((((2 |^ m) - 1) * k) + (((((2 |^ m) - 1) |^ m) - 1) * l)) + s
by A2;
consider f being (s + (((a |^ m) - 1) * k)) + (((b |^ m) - 1) * l) -element natural-valued positive-yielding FinSequence such that
A3:
f is m -solution_of_Sierp167
by Important167, A1;
reconsider f = f as n -element natural-valued positive-yielding FinSequence by A4;
f is m -solution_of_Sierp167
by A3;
hence
ex f being n -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167
; verum