theorem Th13: :: POLYNOM3:13

for n being Element of NAT holds (Decomp (n,2)) . 1 = <*0,n*>