let n0 be natural non zero number ; :: thesis: ( n0 is even implies ex k, m being natural number st
( not m is even & k > 0 & n0 = (2 |^ k) * m ) )
assume A1: n0 is even ; :: thesis: ex k, m being natural number st
( not m is even & k > 0 & n0 = (2 |^ k) * m )
set k = 2 |-count n0;
2 |^ (2 |-count n0) divides n0 by NAT_3:def 7;
then consider m being natural number such that
A2: n0 = (2 |^ (2 |-count n0)) * m by NAT_D:def 3;
take 2 |-count n0 ; :: thesis: ex m being natural number st
( not m is even & 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m )
take m ; :: thesis: ( not m is even & 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m )

A3: now

reconsider m9 = m as Element of NAT by ORDINAL1:def 13;
assume m is even ; :: thesis: contradiction
then consider m99 being Element of NAT such that
A4: m9 = 2 * m99 by ABIAN:def 2;
n0 = ((2 |^ (2 |-count n0)) * 2) * m99 by A2, A4
.= (2 |^ ((2 |-count n0) + 1)) * m99 by NEWTON:11 ;
then 2 |^ ((2 |-count n0) + 1) divides n0 by NAT_D:def 3;
hence contradiction by NAT_3:def 7; :: thesis: verum

end;

hence not m is even ; :: thesis: ( 2 |-count n0 > 0 & n0 = (2 |^ (2 |-count n0)) * m )

now

assume 2 |-count n0 = 0 ; :: thesis: contradiction
then n0 = 1 * m by A2, NEWTON:9;
hence contradiction by A1, A3; :: thesis: verum

end;

hence 2 |-count n0 > 0 ; :: thesis: n0 = (2 |^ (2 |-count n0)) * m
thus n0 = (2 |^ (2 |-count n0)) * m by A2; :: thesis: verum