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