:: deftheorem defines Sierp162FS_2 NUMBER17:def 13 :
for f being complex-valued FinSequence holds Sierp162FS_2 f = <*2,3*> ^ (6 (#) f);