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 A1: ( a = i mod p & b = j mod p ) ; :: thesis: a + b = (i + j) mod p
a + b = ((i mod p) + (j mod p)) mod p by A1, GR_CY_1:def 4;
hence a + b = (i + j) mod p by NAT_D:66; :: thesis: verum