let p be Prime; :: thesis: for i being Element of INT holds i mod p is Element of (GF p)
let i be Element of INT ; :: thesis: i mod p is Element of (GF p)
i mod p in NAT by INT_1:3, INT_1:57;
hence i mod p is Element of (GF p) by INT_1:58, NAT_1:44; :: thesis: verum