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