for k being Nat
for D being non empty set
for pf being FinSequence of D st k in dom pf holds
<*pf*> * (1,k) = pf . k