let a be real number ; :: thesis: a to_power 0 = 1
thus a to_power 0 = a #Z 0 by Def2
.= 1 by PREPOWER:44 ; :: thesis: verum