let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; :: thesis: for x being Element of L holds pow (x,(- 1)) = x "
let x be Element of L; :: thesis: pow (x,(- 1)) = x "
abs (- 1) = - (- 1) by ABSVALUE:def 1;
hence pow (x,(- 1)) = (pow (x,1)) " by Lm3
.= x " by Th14 ;
:: thesis: verum