let L be Field; :: thesis: 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; :: thesis: ( x <> 0. L implies for i being Integer holds pow ((x "),i) = (pow (x,i)) " )

assume A1: x <> 0. L ; :: thesis: for i being Integer holds pow ((x "),i) = (pow (x,i)) "

let i be Integer; :: thesis: pow ((x "),i) = (pow (x,i)) "

for i being Integer holds pow ((x "),i) = (pow (x,i)) "

let x be Element of L; :: thesis: ( x <> 0. L implies for i being Integer holds pow ((x "),i) = (pow (x,i)) " )

assume A1: x <> 0. L ; :: thesis: for i being Integer holds pow ((x "),i) = (pow (x,i)) "

let i be Integer; :: thesis: pow ((x "),i) = (pow (x,i)) "

per cases
( i >= 0 or i < 0 )
;

end;

suppose
i >= 0
; :: thesis: pow ((x "),i) = (pow (x,i)) "

then reconsider n = i as Element of NAT by INT_1:3;

thus pow ((x "),i) = (pow (x,n)) " by A1, Lm9

.= (pow (x,i)) " ; :: thesis: verum

end;thus pow ((x "),i) = (pow (x,n)) " by A1, Lm9

.= (pow (x,i)) " ; :: thesis: verum

suppose A2:
i < 0
; :: thesis: 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 ; :: thesis: verum

end;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 ; :: thesis: verum