let p be Prime; :: thesis: for a being Element of (GF p) holds
( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 )
let a be Element of (GF p); :: thesis: ( a |^ 0 = 1_ (GF p) & a |^ 0 = 1 )
thus A1: a |^ 0 = 1_ (GF p) by BINOM:8; :: thesis: a |^ 0 = 1
p > 1 by INT_2:def 4;
hence a |^ 0 = 1 by A1, INT_3:14; :: thesis: verum