let m, s, k, l, a, b be non zero Nat; :: thesis: ( ex f being s -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 implies ex f being (s + (((a |^ m) - 1) * k)) + (((b |^ m) - 1) * l) -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 )
assume ex f being s -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 ; :: thesis: ex f being (s + (((a |^ m) - 1) * k)) + (((b |^ m) - 1) * l) -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167
then consider f being s -element natural-valued positive-yielding FinSequence such that
B1: f is m -solution_of_Sierp167 ;
defpred S₁[ non zero Nat] means ex f being s + (((a |^ m) - 1) * $1) -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 ;
A1: S₁[1]

proof

reconsider g = Expand (f,m,a) as s + (((a |^ m) - 1) * 1) -element natural-valued positive-yielding FinSequence ;
take g ; :: thesis: g is m -solution_of_Sierp167
thus g is m -solution_of_Sierp167 by B1, Ble1; :: thesis: verum

end;

A2: for l being non zero Nat st S₁[l] holds
S₁[l + 1]

proof

let l be non zero Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume S₁[l] ; :: thesis: S₁[l + 1]
then consider f being s + (((a |^ m) - 1) * l) -element natural-valued positive-yielding FinSequence such that
C1: f is m -solution_of_Sierp167 ;
reconsider g = Expand (f,m,a) as s + (((a |^ m) - 1) * (l + 1)) -element natural-valued positive-yielding FinSequence ;
take g ; :: thesis: g is m -solution_of_Sierp167
thus g is m -solution_of_Sierp167 by C1, Ble1; :: thesis: verum

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A1, A2);
then consider f being s + (((a |^ m) - 1) * k) -element natural-valued positive-yielding FinSequence such that
S1: f is m -solution_of_Sierp167 ;
defpred S₂[ non zero Nat] means ex f being (s + (((a |^ m) - 1) * k)) + (((b |^ m) - 1) * $1) -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 ;
A1: S₂[1]

proof

reconsider g = Expand (f,m,b) as (s + (((a |^ m) - 1) * k)) + (((b |^ m) - 1) * 1) -element natural-valued positive-yielding FinSequence ;
take g ; :: thesis: g is m -solution_of_Sierp167
g is m -solution_of_Sierp167 by S1, Ble1;
hence g is m -solution_of_Sierp167 ; :: thesis: verum

end;

A2: for l being non zero Nat st S₂[l] holds
S₂[l + 1]

proof

let l be non zero Nat; :: thesis: ( S₂[l] implies S₂[l + 1] )
assume S₂[l] ; :: thesis: S₂[l + 1]
then consider f being (s + (((a |^ m) - 1) * k)) + (((b |^ m) - 1) * l) -element natural-valued positive-yielding FinSequence such that
C1: f is m -solution_of_Sierp167 ;
reconsider g = Expand (f,m,b) as (s + (((a |^ m) - 1) * k)) + (((b |^ m) - 1) * (l + 1)) -element natural-valued positive-yielding FinSequence ;
take g ; :: thesis: g is m -solution_of_Sierp167
thus g is m -solution_of_Sierp167 by C1, Ble1; :: thesis: verum

end;

for n being non zero Nat holds S₂[n] from NAT_1:sch 10(A1, A2);
hence ex f being (s + (((a |^ m) - 1) * k)) + (((b |^ m) - 1) * l) -element natural-valued positive-yielding FinSequence st f is m -solution_of_Sierp167 ; :: thesis: verum