theorem Th52: :: POLNOT_1:52

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