A1: 282 * 282 = (1 * ((256 * 256) + 1)) + (71 * 197) ;
(3 |^ 256) * (3 |^ 256) = 3 |^ (256 + 256) by NEWTON:8
.= 3 |^ 512 ;
then (3 |^ (256 * 2)) mod (Fermat 4) = (282 * 282) mod (Fermat 4) by Lm39, NAT_D:67
.= 71 * 197 by A1, Th54, NAT_D:def 2 ;
hence (3 |^ (256 * 2)) mod (Fermat 4) = 71 * 197 ; :: thesis: verum