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 A1: ( a = i mod p & (i * j) mod p = 1 ) ; :: thesis: a " = j mod p
reconsider b = j mod p as Element of (GF p) by Th14;
A2: p > 1 by INT_2:def 4;
A3: b * a = 1 by A1, Th18
.= 1. (GF p) by A2, INT_3:14 ;
then a <> 0. (GF p) ;
hence a " = j mod p by A3, VECTSP_1:def 10; :: thesis: verum