let n be Nat; :: thesis: for K being Ring
for a1, a2, a3 being Element of K st K is commutative holds
((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)
let K be Ring; :: thesis: for a1, a2, a3 being Element of K st K is commutative holds
((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)
let a1, a2, a3 be Element of K; :: thesis: ( K is commutative implies ((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n) )
assume A1: K is commutative ; :: thesis: ((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)
hence ((a1 * a2) * a3) |^ n = ((a1 * a2) |^ n) * (a3 |^ n) by BINOM:9
.= ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n) by A1, BINOM:9 ;
:: thesis: verum