let i be Integer; :: thesis: for p being Prime ex a being Element of (GF p) st a = i mod p
let p be Prime; :: thesis: ex a being Element of (GF p) st a = i mod 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 ALGSEQ_1:1;
hence ex a being Element of (GF p) st a = i mod p ; :: thesis: verum