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