A1: 64 * 64 = (0 * ((256 * 256) + 1)) + (256 * 16) ;
(3 |^ (256 * 16)) * (3 |^ (256 * 16)) = 3 |^ ((256 * 16) + (256 * 16)) by NEWTON:8
.= 3 |^ 8192 ;
then (3 |^ (256 * 32)) mod (Fermat 4) = (64 * 64) mod (Fermat 4) by Lm44, EULER_2:9
.= 256 * 16 by A1, Th59, NAT_D:def 2 ;
hence (3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16 ; :: thesis: verum