A1:
(52 * 289) * (52 * 289) = (3446 * ((256 * 256) + 1)) + 282
;
(3 |^ 256) mod (Fermat 4) =
(3 |^ (128 + 128)) mod (Fermat 4)
.=
((3 |^ 128) * (3 |^ 128)) mod (Fermat 4)
by NEWTON:8
.=
((52 * 289) * (52 * 289)) mod (Fermat 4)
by Lm38, NAT_D:67
.=
282
by A1, Th54, NAT_D:def 2
;
hence
(3 |^ 256) mod (Fermat 4) = 282
; verum