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.|)) "

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.|)) "