let L be Field; :: thesis: 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)))
let x be Element of L; :: thesis: ( x <> 0. L implies 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))) )
assume A1: x <> 0. L ; :: thesis: 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)))
let i, j, k be Nat; :: thesis: (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1)))
(pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,(((i - 1) * (k - 1)) + (- ((j - 1) * (k - 1))))) by A1, Th21
.= pow (x,((i - j) * (k - 1))) ;
hence (pow (x,((i - 1) * (k - 1)))) * (pow (x,(- ((j - 1) * (k - 1))))) = pow (x,((i - j) * (k - 1))) ; :: thesis: verum