theorem Th23: :: POLYNOM8:23

for L being Field
for x being Element of L st x <> 0. L holds
for i, j, k being Nat holds (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1)))