:: deftheorem Def32 defines decomp POLNOT_1:def 32 :
for S being Polish-language
for n being Nat
for p being Element of S ^^ n
for b₄ being FinSequence of S holds
( b₄ = decomp (S,n,p) iff ( dom b₄ = Seg n & ( for m being Nat st m in Seg n holds
ex k being Nat st
( m = k + 1 & b₄ . m = S -head ((S ^^ k) -tail p) ) ) ) );