:: deftheorem defines decomp POLNOT_1:def 31 :
for S being Polish-language
for n, m being Nat
for p being Element of S ^^ ((n + 1) + m) holds decomp (S,n,m,p) = S -head ((S ^^ n) -tail p);