A1: 6561 * 6561 = (656 * ((256 * 256) + 1)) + ((164 * 332) + 1) ;
(3 |^ 16) mod (Fermat 4) = (3 |^ (8 + 8)) mod (Fermat 4)
.= ((3 |^ 8) * (3 |^ 8)) mod (Fermat 4) by NEWTON:8
.= (6561 * 6561) mod (Fermat 4) by Lm34, NAT_D:67
.= (164 * 332) + 1 by A1, Th54, NAT_D:def 2 ;
hence (3 |^ 16) mod (Fermat 4) = (164 * 332) + 1 ; :: thesis: verum