let p be Prime; :: thesis: for g2, a being Element of (GF p) st g2 = 2 mod p holds
(g2 * a) - a = a
let g2, a be Element of (GF p); :: thesis: ( g2 = 2 mod p implies (g2 * a) - a = a )
assume A1: g2 = 2 mod p ; :: thesis: (g2 * a) - a = a
reconsider g1 = 1 mod p as Element of (GF p) by EC_PF_1:14;
A2: g1 = (2 - 1) mod p ;
p > 1 by INT_2:def 4;
then g1 = 1 by NAT_D:63
.= 1. (GF p) by EC_PF_1:12 ;
then (g2 * a) - ((1. (GF p)) * a) = (1. (GF p)) * a by A1, A2, Th21;
then (g2 * a) - a = (1. (GF p)) * a by VECTSP_1:def 6;
hence (g2 * a) - a = a by VECTSP_1:def 6; :: thesis: verum