let L be Field; :: thesis: for j being Integer
for x being Element of L st x <> 0. L holds
pow x,(j + 1) = (pow x,j) * (pow x,1)
let j be Integer; :: thesis: for x being Element of L st x <> 0. L holds
pow x,(j + 1) = (pow x,j) * (pow x,1)
let x be Element of L; :: thesis: ( x <> 0. L implies pow x,(j + 1) = (pow x,j) * (pow x,1) )
A1: pow x,(- 1) = (x |^ (abs (- 1))) " by Def3;
assume A2: x <> 0. L ; :: thesis: pow x,(j + 1) = (pow x,j) * (pow x,1)
then x |^ (abs (- 1)) <> 0. L by Th1;
then A3: pow x,(- 1) <> 0. L by A1, VECTSP_1:74;
A4: pow x,(- j) <> 0. L

proof

per cases ( 0 <= - j or - j < 0 ) ;

suppose 0 <= - j ; :: thesis: pow x,(- j) <> 0. L

then reconsider k = - j as Element of NAT by INT_1:16;
pow x,(- j) = x |^ k by Def3;
hence pow x,(- j) <> 0. L by A2, Th1; :: thesis: verum

end;

suppose A5: - j < 0 ; :: thesis: pow x,(- j) <> 0. L

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

end;

end;

end;

A7: pow x,(j + 1) <> 0. L

proof

per cases ( 0 <= j + 1 or j + 1 < 0 ) ;

suppose 0 <= j + 1 ; :: thesis: pow x,(j + 1) <> 0. L

then reconsider k = j + 1 as Element of NAT by INT_1:16;
pow x,(j + 1) = x |^ k by Def3;
hence pow x,(j + 1) <> 0. L by A2, Th1; :: thesis: verum

end;

suppose A8: j + 1 < 0 ; :: thesis: pow x,(j + 1) <> 0. L

A9: x |^ (abs (j + 1)) <> 0. L by A2, Th1;
pow x,(j + 1) = (x |^ (abs (j + 1))) " by A8, Def3;
hence pow x,(j + 1) <> 0. L by A9, VECTSP_1:74; :: thesis: verum

end;

end;

end;

A10: now

per cases ( j >= 0 or j < - 1 or j = - 1 ) by Lm1;

suppose A11: j >= 0 ; :: thesis: (pow x,(j + 1)) * ((pow x,(- 1)) * (pow x,(- j))) = 1. L

then reconsider n = j as Element of NAT by INT_1:16;
A12: n + 1 = abs (j + 1) by ABSVALUE:def 1;
pow x,(abs j) = x |^ (abs j) by Def3;
then A13: pow x,(abs j) <> 0. L by A2, Th1;
pow x,(abs (j + 1)) = x |^ (abs (j + 1)) by Def3;
then A14: pow x,(abs (j + 1)) <> 0. L by A2, Th1;
n + 1 >= 0 ;
hence (pow x,(j + 1)) * ((pow x,(- 1)) * (pow x,(- j))) = (pow x,(abs (j + 1))) * ((pow x,(- 1)) * (pow x,(- j))) by ABSVALUE:def 1
.= (pow x,(abs (j + 1))) * ((x " ) * (pow x,(- j))) by Th15
.= (pow x,(abs (j + 1))) * ((x " ) * ((pow x,j) " )) by A2, Th18
.= (pow x,(abs (j + 1))) * ((x " ) * ((pow x,(abs j)) " )) by A11, ABSVALUE:def 1
.= (pow x,(abs (j + 1))) * ((x * (pow x,(abs j))) " ) by A2, A13, Th2
.= (pow x,(abs (j + 1))) * ((pow x,((abs j) + 1)) " ) by Th17
.= (pow x,(abs (j + 1))) * ((pow x,(abs (j + 1))) " ) by A12, ABSVALUE:def 1
.= 1. L by A14, VECTSP_1:def 22 ;
:: thesis: verum

end;

suppose A15: j < - 1 ; :: thesis: (pow x,(j + 1)) * ((pow x,(- 1)) * (pow x,(- j))) = 1. L

A16: pow x,(- j) <> 0. L

proof

reconsider k = - j as Element of NAT by A15, INT_1:16;
pow x,(- j) = x |^ k by Def3;
hence pow x,(- j) <> 0. L by A2, Th1; :: thesis: verum

end;

pow x,(abs (j + 1)) = x |^ (abs (j + 1)) by Def3;
then A17: pow x,(abs (j + 1)) <> 0. L by A2, Th1;
A18: j + 1 < (- 1) + 1 by A15, XREAL_1:8;
hence (pow x,(j + 1)) * ((pow x,(- 1)) * (pow x,(- j))) = ((pow x,(abs (j + 1))) " ) * ((pow x,(- 1)) * (pow x,(- j))) by Lm3
.= ((pow x,(abs (j + 1))) " ) * ((x " ) * (pow x,(- j))) by Th15
.= (((pow x,(abs (j + 1))) " ) * (x " )) * (pow x,(- j)) by GROUP_1:def 4
.= (((pow x,(abs (j + 1))) * x) " ) * (pow x,(- j)) by A2, A17, Th2
.= ((pow x,((abs (j + 1)) + 1)) " ) * (pow x,(- j)) by Th17
.= ((pow x,((- (j + 1)) + 1)) " ) * (pow x,(- j)) by A18, ABSVALUE:def 1
.= 1. L by A16, VECTSP_1:def 22 ;
:: thesis: verum

end;

suppose A19: j = - 1 ; :: thesis: (pow x,(j + 1)) * ((pow x,(- 1)) * (pow x,(- j))) = 1. L

A20: x " <> 0. L by A2, VECTSP_1:74;
thus (pow x,(j + 1)) * ((pow x,(- 1)) * (pow x,(- j))) = (1. L) * ((pow x,(- 1)) * (pow x,(- j))) by A19, Th13
.= (pow x,(- 1)) * (pow x,(- j)) by VECTSP_1:def 19
.= (x " ) * (pow x,(- j)) by Th15
.= (x " ) * ((pow x,j) " ) by A2, Th18
.= (x " ) * ((x " ) " ) by A19, Th15
.= 1. L by A20, VECTSP_1:def 22 ; :: thesis: verum

end;

end;

end;

A21: pow x,(j + 1) <> 0. L

proof

per cases ( 0 <= j + 1 or j + 1 < 0 ) ;

suppose 0 <= j + 1 ; :: thesis: pow x,(j + 1) <> 0. L

then reconsider k = j + 1 as Element of NAT by INT_1:16;
pow x,(j + 1) = x |^ k by Def3;
hence pow x,(j + 1) <> 0. L by A2, Th1; :: thesis: verum

end;

suppose A22: j + 1 < 0 ; :: thesis: pow x,(j + 1) <> 0. L

A23: x |^ (abs (j + 1)) <> 0. L by A2, Th1;
pow x,(j + 1) = (x |^ (abs (j + 1))) " by A22, Def3;
hence pow x,(j + 1) <> 0. L by A23, VECTSP_1:74; :: thesis: verum

end;

end;

end;

(pow x,(j + 1)) * (pow x,(- (j + 1))) = (pow x,(j + 1)) * ((pow x,(j + 1)) " ) by A2, Th18
.= 1. L by A7, VECTSP_1:def 22 ;
then A24: pow x,(- (j + 1)) = (pow x,(- 1)) * (pow x,(- j)) by A10, A21, VECTSP_1:33;
thus pow x,(j + 1) = pow x,(- (- (j + 1)))
.= ((pow x,(- 1)) * (pow x,(- j))) " by A2, A24, Th18
.= ((pow x,(- j)) " ) * ((pow x,(- 1)) " ) by A4, A3, Th2
.= (pow x,(- (- j))) * ((pow x,(- 1)) " ) by A2, Th18
.= (pow x,j) * (pow x,(- (- 1))) by A2, Th18
.= (pow x,j) * (pow x,1) ; :: thesis: verum