theorem Th3: :: NAT_6:3

for n being non zero Nat ex k being Nat ex l being odd Nat st n = l * (2 |^ k)