A1: (256 * 16) * (256 * 16) = (255 * ((256 * 256) + 1)) + (673 * 97) ;
(3 |^ (256 * 32)) * (3 |^ (256 * 32)) = 3 |^ ((256 * 32) + (256 * 32)) by NEWTON:13
.= 3 |^ (256 * (32 + 32)) ;
then (3 |^ (256 * 64)) mod (Fermat 4) = ((256 * 16) * (256 * 16)) mod (Fermat 4) by Lm45, EULER_2:11
.= 673 * 97 by A1, Th59, NAT_D:def 2 ;
hence (3 |^ (256 * 64)) mod (Fermat 4) = 673 * 97 ; :: thesis: verum