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:3;
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:3;
A3: pow (x,i) = x |^ m by Def2;
then A4: pow (x,i) <> 0. L by A1, Th1;
A5: pow ((pow (x,i)),j) = ((pow (x,i)) |^ |.j.|) " by A2, Def2;
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:25
.= ((pow ((pow (x,i)),j)) ") " by A1, A3, Th1, Th25
.= pow ((pow (x,i)),j) by A4, A5, Th1, VECTSP_1:24 ;
:: 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:3;
A7: pow (x,i) = (x |^ |.i.|) " by A6, Def2;
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:25
.= pow ((((pow (x,i)) ") "),j) by A1, Th25
.= pow ((pow (x,i)),j) by A1, A7, Th1, VECTSP_1:24 ;
:: 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:3;
A9: pow (x,(- i)) = x |^ m by Def2;
x " <> 0. L by A1, VECTSP_1:25;
then A10: (x ") |^ |.i.| <> 0. L by Th1;
A11: pow ((x "),i) = ((x ") |^ |.i.|) " by A8, Def2;
(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:25
.= pow ((pow (((x ") "),i)),j) by A1, Th25, VECTSP_1:25
.= pow ((pow (x,i)),j) by A1, VECTSP_1:24 ;
:: thesis: verum

end;

end;