theorem Th36: :: FINSEQ_4:36

for p being FinSequence
for x being object
for k being Nat st x in rng p & k in dom (p -| x) holds
p . k = (p -| x) . k