let p be Prime; :: thesis: for a being Element of (GF p) ex n1 being Nat st a = n1 mod p
let a be Element of (GF p); :: thesis: ex n1 being Nat st a = n1 mod p
reconsider a = a as Element of Segm p ;
( 0 <= a & a < p ) by NAT_1:44;
then a = a mod p by NAT_D:63;
hence ex n1 being Nat st a = n1 mod p ; :: thesis: verum