let L be non empty non degenerated right_complementable almost_left_invertible left-distributive well-unital add-associative right_zeroed associative commutative doubleLoopStr ; 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 ; for x being Element of L st x <> 0. L holds
pow ((x "),k) = pow (x,(- k))
let x be Element of L; ( x <> 0. L implies pow ((x "),k) = pow (x,(- k)) )
assume A1:
x <> 0. L
; 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))
; verum