let i, j be Integer; for p being Prime
for gi, gj, gij, a being Element of (GF p) st gi = i mod p & gj = j mod p & gij = (i + j) mod p holds
(gi * a) + (gj * a) = gij * a
let p be Prime; for gi, gj, gij, a being Element of (GF p) st gi = i mod p & gj = j mod p & gij = (i + j) mod p holds
(gi * a) + (gj * a) = gij * a
let gi, gj, gij, a be Element of (GF p); ( gi = i mod p & gj = j mod p & gij = (i + j) mod p implies (gi * a) + (gj * a) = gij * a )
assume A1:
( gi = i mod p & gj = j mod p & gij = (i + j) mod p )
; (gi * a) + (gj * a) = gij * a
(gi + gj) * a = gij * a
by A1, EC_PF_1:15;
hence
(gi * a) + (gj * a) = gij * a
by VECTSP_1:def 7; verum