theorem Th17: :: TOPREAL8:17

for D being non empty set
for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds
(f ^' g) -: (g /. 1) = f