let L be Field; for x being Element of L st x <> 0. L holds
for i being Integer holds pow ((x "),i) = (pow (x,i)) "
let x be Element of L; ( x <> 0. L implies for i being Integer holds pow ((x "),i) = (pow (x,i)) " )
assume A1:
x <> 0. L
; for i being Integer holds pow ((x "),i) = (pow (x,i)) "
let i be Integer; pow ((x "),i) = (pow (x,i)) "
per cases
( i >= 0 or i < 0 )
;
suppose A2:
i < 0
;
pow ((x "),i) = (pow (x,i)) " A3:
pow (
x,
|.i.|)
= x |^ |.i.|
by Def2;
thus pow (
(x "),
i) =
(pow ((x "),|.i.|)) "
by A2, Lm3
.=
pow (
((x ") "),
|.i.|)
by A1, Lm9, VECTSP_1:25
.=
pow (
x,
|.i.|)
by A1, VECTSP_1:24
.=
((pow (x,|.i.|)) ") "
by A1, A3, Th1, VECTSP_1:24
.=
(pow (x,i)) "
by A2, Lm3
;
verum end; end;