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