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) )
assume A1: x <> 0. L ; :: thesis: pow x,(j + 1) = (pow x,j) * (pow x,1)

A2: now

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

suppose A3: 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;
A4: n + 1 >= 0 ;
A5: n + 1 = abs (j + 1) by ABSVALUE:def 1;
A6: pow x,(abs j) <> 0. L

proof

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

end;

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

proof

pow x,(abs (j + 1)) = x |^ (abs (j + 1)) by Def3;
hence pow x,(abs (j + 1)) <> 0. L by A1, Th1; :: thesis: verum

end;

thus (pow x,(j + 1)) * ((pow x,(- 1)) * (pow x,(- j))) = (pow x,(abs (j + 1))) * ((pow x,(- 1)) * (pow x,(- j))) by A4, ABSVALUE:def 1
.= (pow x,(abs (j + 1))) * ((x " ) * (pow x,(- j))) by Th15
.= (pow x,(abs (j + 1))) * ((x " ) * ((pow x,j) " )) by A1, Th18
.= (pow x,(abs (j + 1))) * ((x " ) * ((pow x,(abs j)) " )) by A3, ABSVALUE:def 1
.= (pow x,(abs (j + 1))) * ((x * (pow x,(abs j))) " ) by A1, A6, Th2
.= (pow x,(abs (j + 1))) * ((pow x,((abs j) + 1)) " ) by Th17
.= (pow x,(abs (j + 1))) * ((pow x,(abs (j + 1))) " ) by A5, ABSVALUE:def 1
.= 1. L by A7, VECTSP_1:def 22 ; :: thesis: verum

end;

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

then A9: j + 1 < (- 1) + 1 by XREAL_1:8;
A10: pow x,(abs (j + 1)) <> 0. L

proof

pow x,(abs (j + 1)) = x |^ (abs (j + 1)) by Def3;
hence pow x,(abs (j + 1)) <> 0. L by A1, Th1; :: thesis: verum

end;

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

proof

- j >= - (- 1) by A8, XREAL_1:26;
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 A1, Th1; :: thesis: verum

end;

thus (pow x,(j + 1)) * ((pow x,(- 1)) * (pow x,(- j))) = ((pow x,(abs (j + 1))) " ) * ((pow x,(- 1)) * (pow x,(- j))) by A9, 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 A1, A10, Th2
.= ((pow x,((abs (j + 1)) + 1)) " ) * (pow x,(- j)) by Th17
.= ((pow x,((- (j + 1)) + 1)) " ) * (pow x,(- j)) by A9, ABSVALUE:def 1
.= 1. L by A11, VECTSP_1:def 22 ; :: thesis: verum

end;

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

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

end;

end;

end;

A14: 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 A1, Th1; :: thesis: verum

end;

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

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

end;

end;

end;

A16: 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 A1, Th1; :: thesis: verum

end;

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

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

end;

end;

end;

A18: pow x,(- 1) <> 0. L

proof

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

end;

A20: 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 A1, Th1; :: thesis: verum

end;

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

then A21: pow x,(j + 1) = (x |^ (abs (j + 1))) " by Def3;
x |^ (abs (j + 1)) <> 0. L by A1, Th1;
hence pow x,(j + 1) <> 0. L by A21, 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 A1, Th18
.= 1. L by A14, VECTSP_1:def 22 ;
then A22: pow x,(- (j + 1)) = (pow x,(- 1)) * (pow x,(- j)) by A2, A20, VECTSP_1:33;
thus pow x,(j + 1) = pow x,(- (- (j + 1)))
.= ((pow x,(- 1)) * (pow x,(- j))) " by A1, A22, Th18
.= ((pow x,(- j)) " ) * ((pow x,(- 1)) " ) by A16, A18, Th2
.= (pow x,(- (- j))) * ((pow x,(- 1)) " ) by A1, Th18
.= (pow x,j) * (pow x,(- (- 1))) by A1, Th18
.= (pow x,j) * (pow x,1) ; :: thesis: verum