theorem Th9: :: POLYNOM3:9

for n being Element of NAT holds len (Decomp (n,2)) = n + 1