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 & i = j + 1 holds
(gi * a) - (gj * a) = a
let p be Prime; :: thesis: for gi, gj, a being Element of (GF p) st gi = i mod p & gj = j mod p & i = j + 1 holds
(gi * a) - (gj * a) = a
let gi, gj, a be Element of (GF p); :: thesis: ( gi = i mod p & gj = j mod p & i = j + 1 implies (gi * a) - (gj * a) = a )
assume A1: ( gi = i mod p & gj = j mod p & i = j + 1 ) ; :: thesis: (gi * a) - (gj * a) = a
reconsider g1 = 1 mod p as Element of (GF p) by EC_PF_1:14;
A2: g1 = (i - j) 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 (gi * a) - (gj * a) = (1. (GF p)) * a by A1, A2, Th21;
hence (gi * a) - (gj * a) = a ; :: thesis: verum