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

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

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

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

end;

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

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

end;

end;