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