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