let a be Real; :: 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 |^ |.n.| by Def3
.= a |^ n by ABSVALUE:def 1 ; :: thesis: verum