let i, j be Integer; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: (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; :: thesis: verum