theorem Th3: :: NAT_6:3

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