let p be Prime; :: thesis: for g2, a being Element of (GF p) st g2 = 2 mod p holds
a + a = g2 * a
let g2, a be Element of (GF p); :: thesis: ( g2 = 2 mod p implies a + a = g2 * a )
assume A1: g2 = 2 mod p ; :: thesis: a + a = g2 * a
reconsider g1 = 1 mod p as Element of (GF p) by EC_PF_1:14;
A2: g2 = (1 + 1) mod p by A1;
p > 1 by INT_2:def 4;
then g1 = 1 by NAT_D:63
.= 1. (GF p) by EC_PF_1:12 ;
then ((1. (GF p)) * a) + ((1. (GF p)) * a) = g2 * a by A2, Th18;
then a + ((1. (GF p)) * a) = g2 * a by VECTSP_1:def 6;
hence a + a = g2 * a by VECTSP_1:def 6; :: thesis: verum