let i, k be natural Ordinal; :: thesis: ( i *^ i = 2 *^ k implies ex k being natural Ordinal st i = 2 *^ k )
assume A1: i *^ i = 2 *^ k ; :: thesis: ex k being natural Ordinal st i = 2 *^ k
set id2 = i div^ 2;
{} in 2 by ORDINAL1:14, Lm11;
then A2: i mod^ 2 in 2 by ARYTM_3:6;

per cases ( i mod^ 2 = 0 or i mod^ 2 = 1 ) by A2, Lm11, TARSKI:def 2;

suppose A3: i mod^ 2 = 0 ; :: thesis: ex k being natural Ordinal st i = 2 *^ k

take k = i div^ 2; :: thesis: i = 2 *^ k
thus i = (k *^ 2) +^ 0 by A3, ORDINAL3:65
.= 2 *^ k by ORDINAL2:27 ; :: thesis: verum

end;

suppose i mod^ 2 = 1 ; :: thesis: ex k being natural Ordinal st i = 2 *^ k

then i = ((i div^ 2) *^ 2) +^ 1 by ORDINAL3:65;
then A4: i *^ i = (((i div^ 2) *^ 2) *^ (((i div^ 2) *^ 2) +^ 1)) +^ (one *^ (((i div^ 2) *^ 2) +^ 1)) by ORDINAL3:46
.= (((i div^ 2) *^ 2) *^ (((i div^ 2) *^ 2) +^ 1)) +^ ((one *^ ((i div^ 2) *^ 2)) +^ (one *^ 1)) by ORDINAL3:46
.= (((i div^ 2) *^ 2) *^ (((i div^ 2) *^ 2) +^ 1)) +^ ((one *^ ((i div^ 2) *^ 2)) +^ 1) by ORDINAL2:39
.= ((((i div^ 2) *^ 2) *^ (((i div^ 2) *^ 2) +^ 1)) +^ (one *^ ((i div^ 2) *^ 2))) +^ 1 by ORDINAL3:30
.= (((i div^ 2) *^ 2) *^ ((((i div^ 2) *^ 2) +^ 1) +^ one)) +^ 1 by ORDINAL3:46
.= (((i div^ 2) *^ ((((i div^ 2) *^ 2) +^ 1) +^ one)) *^ 2) +^ 1 by ORDINAL3:50 ;
A5: 1 divides 2 by ARYTM_3:9;
( 2 divides ((i div^ 2) *^ ((((i div^ 2) *^ 2) +^ 1) +^ one)) *^ 2 & 2 divides i *^ i ) by A1;
then 2 divides 1 by A4, ARYTM_3:11;
hence ex k being natural Ordinal st i = 2 *^ k by A5, ARYTM_3:8; :: thesis: verum

end;

end;