(256 * 256) + 1 = (((256 * 256) + 1) * 1) + 0
;
then A1:
((256 * 256) + 1) mod (Fermat 4) = 0
by Th54, NAT_D:def 2;
1 = (((256 * 256) + 1) * 0) + 1
;
then
1 mod (Fermat 4) = 1
by Th54, NAT_D:def 2;
then
((3 |^ ((64 * 0) + (256 * 128))) + 1) mod (Fermat 4) = 0
by A1, Lm46, EULER_2:6;
hence
Fermat 4 divides (3 |^ ((64 * 0) + (256 * 128))) + 1
by Th7, NAT_D:6; verum