theorem Th13: :: EC_PF_2:13

for n being Nat
for K being Field
for a1, a2, a3 being Element of K holds ((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)