for S being Polish-language
for s, t being FinSequence st s is S -headed holds
( s ^ t is S -headed & S -head (s ^ t) = S -head s & S -tail (s ^ t) = (S -tail s) ^ t )