let L be Field; :: thesis: for x being Element of L st x <> 0. L holds
for i, j being Integer holds pow x,(i * j) = pow (pow x,i),j
let x be Element of L; :: thesis: ( x <> 0. L implies for i, j being Integer holds pow x,(i * j) = pow (pow x,i),j )
assume A1: x <> 0. L ; :: thesis: for i, j being Integer holds pow x,(i * j) = pow (pow x,i),j
let i, j be Integer; :: thesis: pow x,(i * j) = pow (pow x,i),j

per cases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( j < 0 & i < 0 ) ) ;

suppose ( i >= 0 & j >= 0 ) ; :: thesis: pow x,(i * j) = pow (pow x,i),j

then reconsider m = i, n = j as Element of NAT by INT_1:16;
thus pow x,(i * j) = pow (pow x,m),n by Th24
.= pow (pow x,i),j ; :: thesis: verum

end;

suppose A2: ( i >= 0 & j < 0 ) ; :: thesis: pow x,(i * j) = pow (pow x,i),j

then reconsider m = i, n = - j as Element of NAT by INT_1:16;
A3: pow x,i = x |^ m by Def3;
then A4: pow x,i <> 0. L by A1, Th1;
A5: pow (pow x,i),j = ((pow x,i) |^ (abs j)) " by A2, Def3;
i * j = - (i * n) ;
hence pow x,(i * j) = (pow x,(i * n)) " by A1, Th18
.= pow (x " ),(i * n) by A1, Th25
.= pow (pow (x " ),m),n by Th24
.= pow ((pow x,i) " ),n by A1, Th25
.= (pow ((pow x,i) " ),j) " by A4, Th18, VECTSP_1:74
.= ((pow (pow x,i),j) " ) " by A1, A3, Th1, Th25
.= pow (pow x,i),j by A4, A5, Th1, VECTSP_1:73 ;
:: thesis: verum

end;

suppose A6: ( i < 0 & j >= 0 ) ; :: thesis: pow x,(i * j) = pow (pow x,i),j

then reconsider m = - i, n = j as Element of NAT by INT_1:16;
A7: pow x,i = (x |^ (abs i)) " by A6, Def3;
i * j = - (m * j) ;
hence pow x,(i * j) = (pow x,(m * j)) " by A1, Th18
.= pow (x " ),(m * j) by A1, Th25
.= pow (pow (x " ),m),n by Th24
.= pow ((pow (x " ),i) " ),n by A1, Th18, VECTSP_1:74
.= pow (((pow x,i) " ) " ),j by A1, Th25
.= pow (pow x,i),j by A1, A7, Th1, VECTSP_1:73 ;
:: thesis: verum

end;

suppose A8: ( j < 0 & i < 0 ) ; :: thesis: pow x,(i * j) = pow (pow x,i),j

then reconsider m = - i, n = - j as Element of NAT by INT_1:16;
A9: pow x,(- i) = x |^ m by Def3;
x " <> 0. L by A1, VECTSP_1:74;
then A10: (x " ) |^ (abs i) <> 0. L by Th1;
A11: pow (x " ),i = ((x " ) |^ (abs i)) " by A8, Def3;
(i * j) * ((- 1) * (- 1)) = m * n ;
hence pow x,(i * j) = pow (pow x,m),n by Th24
.= (pow (pow x,(- i)),j) " by A1, A9, Th1, Th18
.= (pow ((pow x,i) " ),j) " by A1, Th18
.= (pow (pow (x " ),i),j) " by A1, Th25
.= pow ((pow (x " ),i) " ),j by A11, A10, Th25, VECTSP_1:74
.= pow (pow ((x " ) " ),i),j by A1, Th25, VECTSP_1:74
.= pow (pow x,i),j by A1, VECTSP_1:73 ;
:: thesis: verum

end;

end;