A1: ((255 * 256) + 1) * ((255 * 256) + 1) = ((255 * 255) * ((256 * 256) + 1)) + (256 * 256) ;
3 |^ (256 * 128) = (3 |^ (256 * 64)) * (3 |^ (256 * 64))

proof

(3 |^ (256 * 64)) * (3 |^ (256 * 64)) = 3 |^ ((256 * 64) + (256 * 64)) by NEWTON:13
.= 3 |^ (256 * (64 + 64)) ;
hence 3 |^ (256 * 128) = (3 |^ (256 * 64)) * (3 |^ (256 * 64)) ; :: thesis: verum

end;

then (3 |^ (256 * 128)) mod (Fermat 4) = ((673 * 97) * (673 * 97)) mod (Fermat 4) by Lm50, EULER_2:11
.= 256 * 256 by A1, Th59, NAT_D:def 2 ;
hence (3 |^ (256 * 128)) mod (Fermat 4) = 256 * 256 ; :: thesis: verum