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