let i, j be Integer; :: thesis: for p being Prime
for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a * b = (i * j) mod p
let p be Prime; :: thesis: for a, b being Element of (GF p) st a = i mod p & b = j mod p holds
a * b = (i * j) mod p
let a, b be Element of (GF p); :: thesis: ( a = i mod p & b = j mod p implies a * b = (i * j) mod p )
assume ( a = i mod p & b = j mod p ) ; :: thesis: a * b = (i * j) mod p
then a * b = ((i mod p) * (j mod p)) mod p by INT_3:def 10;
hence a * b = (i * j) mod p by NAT_D:67; :: thesis: verum