theorem Th6: :: GLIB_006:4

for f, g being FinSequence
for i being Nat st i <= len f & mid (f,i,((i -' 1) + (len g))) = g holds
(i -' 1) + (len g) <= len f