A1: 2 |^ 2 = 2 |^ (1 + 1)
.= (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 ;
3 = (2 * 1) + 1 ;
then reconsider e = 3 as odd Nat ;
take e ; :: according to NAT_6:def 5 :: thesis: ex n being positive Nat st
( 2 |^ n > e & 13 = (e * (2 |^ n)) + 1 )
take 2 ; :: thesis: ( 2 |^ 2 > e & 13 = (e * (2 |^ 2)) + 1 )
thus ( 2 |^ 2 > e & 13 = (e * (2 |^ 2)) + 1 ) by A1; :: thesis: verum