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) "
A2: x " <> 0. L by A1, VECTSP_1:74;

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 A3: i < 0 ; :: thesis: pow (x " ),i = (pow x,i) "

A4: pow x,(abs i) <> 0. L

proof

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

end;

thus pow (x " ),i = (pow (x " ),(abs i)) " by A3, Lm3
.= pow ((x " ) " ),(abs i) by A2, Lm9
.= pow x,(abs i) by A1, VECTSP_1:73
.= ((pow x,(abs i)) " ) " by A4, VECTSP_1:73
.= (pow x,i) " by A3, Lm3 ; :: thesis: verum

end;

end;