let n be non zero Nat; :: thesis: ex k being Nat ex l being odd Nat st n = l * (2 |^ k)
consider a, b being Nat such that
A1: n = (2 |^ a) * ((2 * b) + 1) by NAGATA_2:1;
take a ; :: thesis: ex l being odd Nat st n = l * (2 |^ a)
take (2 * b) + 1 ; :: thesis: n = ((2 * b) + 1) * (2 |^ a)
thus n = ((2 * b) + 1) * (2 |^ a) by A1; :: thesis: verum