theorem Th20: :: POLYNOM8:20
for L being Field
for j being Integer
for x being Element of L st x <> 0. L holds
pow (x,(j - 1)) = (pow (x,j)) * (pow (x,(- 1)))