let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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:24;

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

hence pow (x,(- i)) = (pow (x,|.(- 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 10
.= (1. L) "
.= (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,|.i.|) = x |^ |.i.| by Def2;
pow (x,i) = (pow (x,|.i.|)) " by A6, Lm3;
then (pow (x,i)) " = pow (x,|.i.|) by A1, A7, Th1, VECTSP_1:24;
hence (pow (x,i)) " = pow (x,(- i)) by A6, ABSVALUE:def 1; :: thesis: verum

end;

end;