let n, k be Element of NAT ; :: thesis: ( n > 0 implies n ^ (- (k + 1)) = (n ^ (- k)) / n )
assume A1: n > 0 ; :: thesis: n ^ (- (k + 1)) = (n ^ (- k)) / n
thus n ^ (- (k + 1)) = n ^ ((- k) - 1)
.= (n ^ (- k)) / (n ^ 1) by A1, POWER:34
.= (n ^ (- k)) / n by POWER:30 ; :: thesis: verum