theorem Th145: :: NUMBER17:145

for s being positive Nat
for f being b₁ + 1 -element complex-valued FinSequence st f is a_solution_of_Sierp169 holds
(10 (#) (f | (s - 1))) ^ <*(12 * (f . s)),(15 * (f . s)),(20 * (f . s)),(10 * (f . (s + 1)))*> is a_solution_of_Sierp169