:: deftheorem defines ^^ POLNOT_1:def 4 :
for P being FinSequence-membered set
for n being Nat holds P ^^ n = (P ^^) . n;