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)) "

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

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

then reconsider n = i as Element of NAT by INT_1:16;
thus pow ((x "),i) = (pow (x,n)) " by A1, Lm9
.= (pow (x,i)) " ; :: thesis: verum

end;

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

A3: pow (x,(abs i)) = x |^ (abs i) by Def3;
thus pow ((x "),i) = (pow ((x "),(abs i))) " by A2, Lm3
.= pow (((x ") "),(abs i)) by A1, Lm9, VECTSP_1:74
.= pow (x,(abs i)) by A1, VECTSP_1:73
.= ((pow (x,(abs i))) ") " by A1, A3, Th1, VECTSP_1:73
.= (pow (x,i)) " by A2, Lm3 ; :: thesis: verum

end;

end;