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