A1: 81 = (0 * ((256 * 256) + 1)) + 81 ;
thus (3 |^ 4) mod (Fermat 4) = (3 |^ (2 + 2)) mod (Fermat 4)
.= ((3 |^ 2) * (3 |^ 2)) mod (Fermat 4) by NEWTON:8
.= (9 * 9) mod (Fermat 4) by Lm32, NAT_D:67
.= 81 by A1, Th54, NAT_D:def 2 ; :: thesis: verum