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 ( i >= 0 & - j >= - 0 ) ;
then reconsider m = i, n = - j as Element of NAT by INT_1:16;
A3: i * j = - (i * n) ;
A4: pow x,i <> 0. L

proof

pow x,i = x |^ m by Def3;
hence pow x,i <> 0. L by A1, Th1; :: thesis: verum

end;

then A5: (pow x,i) " <> 0. L by VECTSP_1:74;
A6: pow (pow x,i),j <> 0. L

proof

A7: pow (pow x,i),j = ((pow x,i) |^ (abs j)) " by A2, Def3;
(pow x,i) |^ (abs j) <> 0. L by A4, Th1;
hence pow (pow x,i),j <> 0. L by A7, VECTSP_1:74; :: thesis: verum

end;

thus pow x,(i * j) = (pow x,(i * n)) " by A1, A3, 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 A5, Th18
.= ((pow (pow x,i),j) " ) " by A4, Th25
.= pow (pow x,i),j by A6, VECTSP_1:73 ; :: thesis: verum

end;

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

then ( - i >= - 0 & j >= 0 ) ;
then reconsider m = - i, n = j as Element of NAT by INT_1:16;
A9: i * j = - (m * j) ;
A10: x " <> 0. L by A1, VECTSP_1:74;
A11: pow x,i <> 0. L

proof

A12: pow x,i = (x |^ (abs i)) " by A8, Def3;
x |^ (abs i) <> 0. L by A1, Th1;
hence pow x,i <> 0. L by A12, VECTSP_1:74; :: thesis: verum

end;

thus pow x,(i * j) = (pow x,(m * j)) " by A1, A9, Th18
.= pow (x " ),(m * j) by A1, Th25
.= pow (pow (x " ),m),n by Th24
.= pow ((pow (x " ),i) " ),n by A10, Th18
.= pow (((pow x,i) " ) " ),j by A1, Th25
.= pow (pow x,i),j by A11, VECTSP_1:73 ; :: thesis: verum

end;

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

then ( - j >= - 0 & - i >= - 0 ) ;
then reconsider m = - i, n = - j as Element of NAT by INT_1:16;
A14: (i * j) * ((- 1) * (- 1)) = m * n ;
A15: pow x,(- i) <> 0. L

proof

pow x,(- i) = x |^ m by Def3;
hence pow x,(- i) <> 0. L by A1, Th1; :: thesis: verum

end;

A16: pow (x " ),i <> 0. L

proof

A17: pow (x " ),i = ((x " ) |^ (abs i)) " by A13, Def3;
x " <> 0. L by A1, VECTSP_1:74;
then (x " ) |^ (abs i) <> 0. L by Th1;
hence pow (x " ),i <> 0. L by A17, VECTSP_1:74; :: thesis: verum

end;

A18: x " <> 0. L by A1, VECTSP_1:74;
thus pow x,(i * j) = pow (pow x,m),n by A14, Th24
.= (pow (pow x,(- i)),j) " by A15, Th18
.= (pow ((pow x,i) " ),j) " by A1, Th18
.= (pow (pow (x " ),i),j) " by A1, Th25
.= pow ((pow (x " ),i) " ),j by A16, Th25
.= pow (pow ((x " ) " ),i),j by A18, Th25
.= pow (pow x,i),j by A1, VECTSP_1:73 ; :: thesis: verum

end;

end;