let a be Real; :: thesis: for k being Integer holds (1 / a) #Z k = 1 / (a #Z k)
let k be Integer; :: thesis: (1 / a) #Z k = 1 / (a #Z k)

per cases ( k >= 0 or k < 0 ) ;

suppose A1: k >= 0 ; :: thesis: (1 / a) #Z k = 1 / (a #Z k)

hence (1 / a) #Z k = (1 / a) |^ |.k.| by Def3
.= 1 / (a |^ |.k.|) by Th7
.= 1 / (a #Z k) by A1, Def3 ;
:: thesis: verum

end;

suppose A2: k < 0 ; :: thesis: (1 / a) #Z k = 1 / (a #Z k)

hence (1 / a) #Z k = ((1 / a) |^ |.k.|) " by Def3
.= (1 / (a |^ |.k.|)) " by Th7
.= ((a |^ |.k.|) ") "
.= (a #Z k) " by A2, Def3
.= 1 / (a #Z k) ;
:: thesis: verum

end;

end;