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) & - (- 1) = 1 ) by ABSVALUE:def 1;
hence pow x,(- 1) = (pow x,1) " by Lm3
.= x " by Th14 ;
:: thesis: verum