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 22
.= (1_ L) " by VECTSP_1:def 19
.= (x |^ 0 ) " by BINOM:8
.= (x |^ (abs i)) " by A3, ABSVALUE:def 1
.= (pow x,(abs i)) " by Def3 ;
:: thesis: verum

end;

end;