A1: (123 * 503) * (123 * 503) = ((325 + (241 * 241)) * ((256 * 256) + 1)) + ((14 * 1367) + 1) ;
(3 |^ 64) mod (Fermat 4) = (3 |^ (32 + 32)) mod (Fermat 4)
.= ((3 |^ 32) * (3 |^ 32)) mod (Fermat 4) by NEWTON:8
.= ((123 * 503) * (123 * 503)) mod (Fermat 4) by Lm36, NAT_D:67
.= (14 * 1367) + 1 by A1, Th54, NAT_D:def 2 ;
hence (3 |^ 64) mod (Fermat 4) = (14 * 1367) + 1 ; :: thesis: verum