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