theorem :: FINSEQ_4:15

for i being Nat
for D being set
for P being FinSequence of D st 1 <= i & i <= len P holds
P /. i = P . i