theorem Th15: :: TOPREAL8:15

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 = (1,((len f) -' 1)) -cut f