let a be non zero Nat; :: thesis: ex k being odd Nat st a = (2 |^ (2 |-count a)) * k
A1: not 2 is trivial ;
then consider k being Nat such that
A2: a = (2 |^ (2 |-count a)) * k by LmC1, NAT_D:def 3;
not 2 * (2 |^ (2 |-count a)) divides (2 |^ (2 |-count a)) * k by A1, A2, LmC1;
then k is odd by NEWTON02:2;
hence ex k being odd Nat st a = (2 |^ (2 |-count a)) * k by A2; :: thesis: verum