:: deftheorem defines * POLNOT_1:def 5 :
for P being FinSequence-membered set holds P * = union { (P ^^ n) where n is Nat : verum } ;