let a be real number ; :: 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) |^ (abs k) by Def3
.= 1 / (a |^ (abs 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) |^ (abs k)) " by Def3
.= (1 / (a |^ (abs k))) " by Th7
.= ((a |^ (abs k)) ") "
.= (a #Z k) " by A2, Def3
.= 1 / (a #Z k) ;
:: thesis: verum

end;

end;