let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; 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; for i being Integer st 0 > i holds
pow (a,i) = (pow (a,|.i.|)) "
let i be Integer; ( 0 > i implies pow (a,i) = (pow (a,|.i.|)) " )
assume A1:
0 > i
; 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; verum