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