let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ; :: thesis: for x being Element of L holds pow (x,(- 1)) = x "

let x be Element of L; :: thesis: pow (x,(- 1)) = x "

|.(- 1).| = - (- 1) by ABSVALUE:def 1;

hence pow (x,(- 1)) = (pow (x,1)) " by Lm3

.= x " by Th14 ;

:: thesis: verum

let x be Element of L; :: thesis: pow (x,(- 1)) = x "

|.(- 1).| = - (- 1) by ABSVALUE:def 1;

hence pow (x,(- 1)) = (pow (x,1)) " by Lm3

.= x " by Th14 ;

:: thesis: verum