:: deftheorem Def102 defines FlattenSeq POLNOT_1:def 44 :
for S being Polish-language
for p being FinSequence of S
for b₃ being Element of S ^^ (len p) holds
( b₃ = FlattenSeq p iff decomp (S,(len p),b₃) = p );