let n be Nat; :: thesis: for K being Field
for a1, a2, a3 being Element of K holds ((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)
let K be Field; :: thesis: for a1, a2, a3 being Element of K holds ((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)
let a1, a2, a3 be Element of K; :: thesis: ((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)
thus ((a1 * a2) * a3) |^ n = ((a1 * a2) |^ n) * (a3 |^ n) by BINOM:9
.= ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n) by BINOM:9 ; :: thesis: verum