let x be Real; :: thesis: for n being Nat holds (1 / x) #Z n = 1 / (x #Z n)
let n be Nat; :: thesis: (1 / x) #Z n = 1 / (x #Z n)
(1 / x) #Z n = (1 / x) |^ n by PREPOWER:36
.= 1 / (x |^ n) by PREPOWER:7 ;
hence (1 / x) #Z n = 1 / (x #Z n) by PREPOWER:36; :: thesis: verum