theorem Th57: :: POLNOT_1:57

for S being Polish-language
for m, n being Nat
for s being FinSequence st m + 1 <= n & s in S ^^ n holds
( s is S ^^ m -headed & (S ^^ m) -tail s is S -headed )