let k, n be 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:29
.= (n ^ (- k)) / n ; :: thesis: verum