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