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 |^ |.(- 1).|) " by Def2;
assume A2: x <> 0. L ; :: thesis: pow (x,(j + 1)) = (pow (x,j)) * (pow (x,1))
then x |^ |.(- 1).| <> 0. L by Th1;
then A3: pow (x,(- 1)) <> 0. L by A1, VECTSP_1:25;
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:3;
pow (x,(- j)) = x |^ k by Def2;
hence pow (x,(- j)) <> 0. L by A2, Th1; :: thesis: verum

end;

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

A6: x |^ |.(- j).| <> 0. L by A2, Th1;
pow (x,(- j)) = (x |^ |.(- j).|) " by A5, Def2;
hence pow (x,(- j)) <> 0. L by A6, VECTSP_1:25; :: 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:3;
pow (x,(j + 1)) = x |^ k by Def2;
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 |^ |.(j + 1).| <> 0. L by A2, Th1;
pow (x,(j + 1)) = (x |^ |.(j + 1).|) " by A8, Def2;
hence pow (x,(j + 1)) <> 0. L by A9, VECTSP_1:25; :: thesis: verum

end;

end;

end;

A10: now :: thesis: (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = 1. L

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:3;
A12: n + 1 = |.(j + 1).| by ABSVALUE:def 1;
pow (x,|.j.|) = x |^ |.j.| by Def2;
then A13: pow (x,|.j.|) <> 0. L by A2, Th1;
pow (x,|.(j + 1).|) = x |^ |.(j + 1).| by Def2;
then A14: pow (x,|.(j + 1).|) <> 0. L by A2, Th1;
n + 1 >= 0 ;
hence (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = (pow (x,|.(j + 1).|)) * ((pow (x,(- 1))) * (pow (x,(- j)))) by ABSVALUE:def 1
.= (pow (x,|.(j + 1).|)) * ((x ") * (pow (x,(- j)))) by Th15
.= (pow (x,|.(j + 1).|)) * ((x ") * ((pow (x,j)) ")) by A2, Th18
.= (pow (x,|.(j + 1).|)) * ((x ") * ((pow (x,|.j.|)) ")) by A11, ABSVALUE:def 1
.= (pow (x,|.(j + 1).|)) * ((x * (pow (x,|.j.|))) ") by A2, A13, Th2
.= (pow (x,|.(j + 1).|)) * ((pow (x,(|.j.| + 1))) ") by Th17
.= (pow (x,|.(j + 1).|)) * ((pow (x,|.(j + 1).|)) ") by A12, ABSVALUE:def 1
.= 1. L by A14, VECTSP_1:def 10 ;
:: 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:3;
pow (x,(- j)) = x |^ k by Def2;
hence pow (x,(- j)) <> 0. L by A2, Th1; :: thesis: verum

end;

pow (x,|.(j + 1).|) = x |^ |.(j + 1).| by Def2;
then A17: pow (x,|.(j + 1).|) <> 0. L by A2, Th1;
A18: j + 1 < (- 1) + 1 by A15, XREAL_1:6;
hence (pow (x,(j + 1))) * ((pow (x,(- 1))) * (pow (x,(- j)))) = ((pow (x,|.(j + 1).|)) ") * ((pow (x,(- 1))) * (pow (x,(- j)))) by Lm3
.= ((pow (x,|.(j + 1).|)) ") * ((x ") * (pow (x,(- j)))) by Th15
.= (((pow (x,|.(j + 1).|)) ") * (x ")) * (pow (x,(- j))) by GROUP_1:def 3
.= (((pow (x,|.(j + 1).|)) * x) ") * (pow (x,(- j))) by A2, A17, Th2
.= ((pow (x,(|.(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 10 ;
:: 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:25;
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)))
.= (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 10 ; :: 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:3;
pow (x,(j + 1)) = x |^ k by Def2;
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 |^ |.(j + 1).| <> 0. L by A2, Th1;
pow (x,(j + 1)) = (x |^ |.(j + 1).|) " by A22, Def2;
hence pow (x,(j + 1)) <> 0. L by A23, VECTSP_1:25; :: 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 10 ;
then A24: pow (x,(- (j + 1))) = (pow (x,(- 1))) * (pow (x,(- j))) by A10, A21, VECTSP_1:5;
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