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

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