theorem :: MATRIXJ1:5

for n being Nat
for K being Field
for a being Element of K holds Product (n |-> a) = (power K) . (a,n)