let i be Integer; :: thesis: for p being Prime holds i mod p is Element of (GF p)
let p be Prime; :: thesis: i mod p is Element of (GF p)
reconsider b = i mod p as Integer ;
b in NAT by INT_1:3, INT_1:57;
then reconsider b = b as Nat ;
b < p by INT_1:58;
then b in Segm p by NAT_1:44;
hence i mod p is Element of (GF p) ; :: thesis: verum