let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for i being Integer
for x being Element of L st x <> 0. L holds
(pow x,i) " = pow x,(- i)
let i be Integer; :: thesis: for x being Element of L st x <> 0. L holds
(pow x,i) " = pow x,(- i)
let x be Element of L; :: thesis: ( x <> 0. L implies (pow x,i) " = pow x,(- i) )
assume A1: x <> 0. L ; :: thesis: (pow x,i) " = pow x,(- i)
A2: 1. L <> 0. L ;

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

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

per cases ( - i < - 0 or i = 0 ) by A3, XREAL_1:26;

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

hence pow x,(- i) = (pow x,(abs (- i))) " by Lm3
.= (pow x,(- (- i))) " by A4, ABSVALUE:def 1
.= (pow x,i) " ;
:: thesis: verum

end;

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

hence pow x,(- i) = 1. L by Th13
.= (1. L) * ((1. L) " ) by A2, VECTSP_1:def 22
.= (1. L) " by VECTSP_1:def 19
.= (pow x,i) " by A5, Th13 ;
:: thesis: verum

end;

end;

end;

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

A7: 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;

pow x,i = (pow x,(abs i)) " by A6, Lm3;
then ( (pow x,i) " = pow x,(abs i) & abs i = - i ) by A6, A7, ABSVALUE:def 1, VECTSP_1:73;
hence (pow x,i) " = pow x,(- i) ; :: thesis: verum

end;

end;