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

per cases ( i < 0 or i = 0 ) by A2;

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

hence pow (x,i) = (pow (x,(abs i))) " by Lm3; :: thesis: verum

end;

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

hence pow (x,i) = 1. L by Th13
.= (1. L) * ((1. L) ") by A1, VECTSP_1:def 10
.= (1_ L) " by VECTSP_1:def 8
.= (x |^ 0) " by BINOM:8
.= (x |^ (abs i)) " by A3, ABSVALUE:def 1
.= (pow (x,(abs i))) " by Def3 ;
:: thesis: verum

end;

end;