(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, NAT_D:66;
hence Fermat 4 divides (3 |^ ((64 * 0) + (256 * 128))) + 1 by Th7, NAT_D:6; :: thesis: verum