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