theorem Th56: :: FINSEQ_6:56

for k being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > k holds
p .. f = k + (p .. (f /^ k))