let p be Prime; :: thesis: for a being Element of (GF p) holds (power (GF p)) . (a,1) = a
let a be Element of (GF p); :: thesis: (power (GF p)) . (a,1) = a
consider b being Element of (GF p) such that
P0: b = (power (GF p)) . (a,0) ;
(power (GF p)) . (a,(0 + 1)) = b * a by P0, GROUP_1:def 7
.= (1_ (GF p)) * a by P0, GROUP_1:def 7
.= a by GROUP_1:def 4 ;
hence (power (GF p)) . (a,1) = a ; :: thesis: verum