let i, j be Integer; :: thesis: for p being Prime
for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds
a " = j mod p
let p be Prime; :: thesis: for a being Element of (GF p) st a = i mod p & (i * j) mod p = 1 holds
a " = j mod p
let a be Element of (GF p); :: thesis: ( a = i mod p & (i * j) mod p = 1 implies a " = j mod p )
assume AS: ( a = i mod p & (i * j) mod p = 1 ) ; :: thesis: a " = j mod p
consider b being Element of (GF p) such that
P0: b = j mod p by GF2;
P1: p > 1 by INT_2:def 4;
P3: b * a = 1 by AS, P0, GF6
.= 1. (GF p) by P1, INT_3:14 ;
then a <> 0. (GF p) by VECTSP_1:7;
hence a " = j mod p by P0, P3, VECTSP_1:def 10; :: thesis: verum