let p be Prime; :: thesis: 1 = 1. (GF p)
1 < p by INT_2:def 4;
then 1 in Segm p by NAT_1:44;
hence 1 = 1. (GF p) by FUNCT_7:def 1; :: thesis: verum