:: deftheorem defines Sierp162FS NUMBER17:def 12 :
for f being complex-valued FinSequence holds Sierp162FS f = <*2*> ^ (2 (#) f);