let G be GaloisField of q; :: thesis: ( G is p -characteristic & G is Z/ p -extending )
Z/ p is Subfield of G by defGal;
then Z/ p is Subring of G by FIELD_5:12;
then Char G = Char (Z/ p) by RING_3:89
.= p by RING_3:77 ;
hence G is p -characteristic by RING_3:def 6; :: thesis: G is Z/ p -extending
Z/ p is Subfield of G by defGal;
hence G is Z/ p -extending by FIELD_4:7; :: thesis: verum