let k be Nat; :: thesis: for a being non zero Real holds (a to_power k) * (a to_power (- k)) = 1
let a be non zero Real; :: thesis: (a to_power k) * (a to_power (- k)) = 1
(a to_power k) * (a to_power (- k)) = (a #Z k) * (a to_power (- k)) by POWER:def 2
.= (a #Z k) * (a #Z (- k)) by POWER:def 2
.= a #Z (k + (- k)) by PREPOWER:44
.= 1 by PREPOWER:34 ;
hence (a to_power k) * (a to_power (- k)) = 1 ; :: thesis: verum