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