theorem Th58: :: POLNOT_1:58

for S being Polish-language
for s being FinSequence holds
( s is S ^^ 0 -headed & (S ^^ 0) -head s = {} & (S ^^ 0) -tail s = s )