theorem Th53: :: POLNOT_1:53

for S being Polish-language
for s being FinSequence st s in S holds
( S -head s = s & S -tail s = {} )