let a be real number ; :: thesis: for n being natural number holds a #Z n = a |^ n
let n be natural number ; :: thesis: a #Z n = a |^ n
thus a #Z n = a |^ (abs n) by Def4
.= a |^ n by ABSVALUE:def 1 ; :: thesis: verum