theorem Th5: :: TOPREAL8:5

for p being set
for D being non empty set
for f being non empty FinSequence of D
for g being FinSequence of D st p .. f = len f holds
(f ^ g) |-- p = g