theorem Th62: :: POLNOT_1:62

for S being Polish-language
for n being Nat
for q being Element of S ^^ n holds len (decomp (S,n,q)) = n