let L be non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed 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 Def3
.= (x |^ k) " by A1, Lm8
.= (pow x,k) " by Def3
.= pow x,(- k) by A1, Th18 ;
hence pow (x " ),k = pow x,(- k) ; :: thesis: verum