let n1, n2 be Nat; :: thesis: for p being Prime
for a being Element of (GF p) holds (a |^ n1) |^ n2 = a |^ (n1 * n2)
let p be Prime; :: thesis: for a being Element of (GF p) holds (a |^ n1) |^ n2 = a |^ (n1 * n2)
let a be Element of (GF p); :: thesis: (a |^ n1) |^ n2 = a |^ (n1 * n2)
( n1 in NAT & n2 in NAT ) by ORDINAL1:def 12;
hence (a |^ n1) |^ n2 = a |^ (n1 * n2) by BINOM:11; :: thesis: verum