let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; :: thesis: for a being Element of L
for i being Integer st 0 > i holds
pow (a,i) = (pow (a,(abs i))) "
let a be Element of L; :: thesis: for i being Integer st 0 > i holds
pow (a,i) = (pow (a,(abs i))) "
let i be Integer; :: thesis: ( 0 > i implies pow (a,i) = (pow (a,(abs i))) " )
assume A1: 0 > i ; :: thesis: pow (a,i) = (pow (a,(abs i))) "
pow (a,(abs i)) = (power L) . (a,(abs i)) by Def3;
hence pow (a,i) = (pow (a,(abs i))) " by A1, Def3; :: thesis: verum