let k be Nat; :: thesis: for a being non empty real number holds (a to_power k) * (a to_power (- k)) = 1
let a be non empty real number ; :: 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:54
.= 1 by PREPOWER:44 ;
hence (a to_power k) * (a to_power (- k)) = 1 ; :: thesis: verum