A1: 2 |^ 2 = 2 |^ (1 + 1)
.= (2 |^ 1) * 2 by NEWTON:6
.= 2 * 2 ;
then 2 |^ (2 + 2) = 4 * 4 by NEWTON:8;
then 2 |^ (4 + 4) = 16 * 16 by NEWTON:8;
then A2: 2 |^ (8 + 2) = 256 * 4 by A1, NEWTON:8;
A3: 13 = (2 * 6) + 1 ;
13313 = (13 * (2 |^ 10)) + 1 by A2;
hence 13313 is Proth by A2, A3; :: thesis: verum