thus z `1 is Element of (GF p) ; :: thesis: verum