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