:: deftheorem defines [#] SETWOP_2:def 1 :
for D being non empty set
for p being FinSequence of D
for d being Element of D holds [#] (p,d) = (NAT --> d) +* p;