let s be positive Nat; :: thesis: for f being s + 1 -element natural-valued positive FinSequence st f is a_solution_of_Sierp169 holds
ex g being (s + 2) + 1 -element natural-valued positive FinSequence st g is a_solution_of_Sierp169
let f be s + 1 -element natural-valued positive FinSequence; :: thesis: ( f is a_solution_of_Sierp169 implies ex g being (s + 2) + 1 -element natural-valued positive FinSequence st g is a_solution_of_Sierp169 )
set g = (10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*>;
assume A1: f is a_solution_of_Sierp169 ; :: thesis: ex g being (s + 2) + 1 -element natural-valued positive FinSequence st g is a_solution_of_Sierp169
reconsider g = (10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*> as (s + 2) + 1 -element natural-valued positive FinSequence ;
take g ; :: thesis: g is a_solution_of_Sierp169
thus g is a_solution_of_Sierp169 by A1, Th145; :: thesis: verum