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