let a be Real; :: thesis: a to_power 1 = a
thus a to_power 1 = a #Z 1 by Def2
.= a by PREPOWER:35 ; :: thesis: verum