let a be Real; :: thesis: 1 to_power a = 1
A1: 1 #R a <> 0 by PREPOWER:81;
thus 1 to_power a = (1 / 1) #R a by Def2
.= (1 #R a) / (1 #R a) by PREPOWER:80
.= 1 by A1, XCMPLX_1:60 ; :: thesis: verum