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