theorem Th13: :: EC_PF_2:13

for n being Nat
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)