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