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 Lm43, NAT_D:67
.= 256 * 16 by A1, Th54, NAT_D:def 2 ;
hence (3 |^ (256 * 32)) mod (Fermat 4) = 256 * 16 ; :: thesis: verum