:: deftheorem defines SierpProblem168FS NUMBER15:def 13 :
for s being positive Nat
for f being b₁ + 1 -element complex-valued FinSequence holds SierpProblem168FS f = (12 (#) (f | (s - 1))) ^ <*(15 * (f . s)),(20 * (f . s)),(12 * (f . (s + 1)))*>;