for D being non empty set
for d being Element of D
for i being Nat
for p being FinSequence of D holds
( ( i in dom p implies ([#] (p,d)) . i = p . i ) & ( not i in dom p implies ([#] (p,d)) . i = d ) )