theorem :: SETWOP_2:21

for D being non empty set
for d being Element of D
for p being FinSequence of D holds ([#] (p,d)) | (dom p) = p