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
gj + gij = (j + (i - j)) mod p by A1, EC_PF_1:15
.= gi by A1 ;
then ((gj * a) + (gij * a)) - (gj * a) = (gi * a) - (gj * a) by VECTSP_1:def 7;
then (gij * a) + ((gj * a) + (- (gj * a))) = (gi * a) - (gj * a) by ALGSTR_1:7;
then (gij * a) + (0. (GF p)) = (gi * a) - (gj * a) by VECTSP_1:19;
hence (gi * a) - (gj * a) = gij * a by ALGSTR_1:7; :: thesis: verum