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