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