let L be non empty non degenerated right_complementable almost_left_invertible left-distributive well-unital add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for k being Element of NAT
for x being Element of L st x <> 0. L holds
pow ((x "),k) = pow (x,(- k))
let k be Element of NAT ; :: thesis: for x being Element of L st x <> 0. L holds
pow ((x "),k) = pow (x,(- k))
let x be Element of L; :: thesis: ( x <> 0. L implies pow ((x "),k) = pow (x,(- k)) )
assume A1: x <> 0. L ; :: thesis: pow ((x "),k) = pow (x,(- k))
pow ((x "),k) = (x ") |^ k by Def2
.= (x |^ k) " by A1, Lm8
.= (pow (x,k)) " by Def2
.= pow (x,(- k)) by A1, Th18 ;
hence pow ((x "),k) = pow (x,(- k)) ; :: thesis: verum