let p be Prime; :: thesis: for n being Nat st n in Seg p holds
n - 1 is Element of (GF p)
let n be Nat; :: thesis: ( n in Seg p implies n - 1 is Element of (GF p) )
assume n in Seg p ; :: thesis: n - 1 is Element of (GF p)
then ( 1 <= n & n <= p ) by FINSEQ_1:1;
then A1: ( 1 - 1 <= n - 1 & n - 1 <= p - 1 ) by XREAL_1:9;
then A2: n - 1 is Element of NAT by INT_1:3;
p - 1 < p - 0 by XREAL_1:15;
then n - 1 < p by A1, XXREAL_0:2;
hence n - 1 is Element of (GF p) by A2, NAT_1:44; :: thesis: verum