let x be Real; :: thesis: for n being natural number holds (1 / x) #Z n = 1 / (x #Z n)
let n be natural number ; :: thesis: (1 / x) #Z n = 1 / (x #Z n)
(1 / x) #Z n = (1 / x) |^ n by PREPOWER:46
.= 1 / (x |^ n) by PREPOWER:14 ;
hence (1 / x) #Z n = 1 / (x #Z n) by PREPOWER:46; :: thesis: verum