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