theorem Th15: :: FINSEQ_5:15

for D being non empty set
for p being Element of D
for f being FinSequence of D holds (<*p*> ^ f) /. 1 = p