theorem Th54: :: POLNOT_1:54

for S, T being Polish-language
for u being FinSequence st u in S ^ T holds
( S -head u in S & S -tail u in T )