thus a to_power n = a #Z n by Def2
.= a |^ n by PREPOWER:36 ; :: thesis: verum