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 Def4
.= 1 / (a |^ (abs k)) by Th14
.= 1 / (a #Z k) by A1, Def4 ;
:: 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 Def4
.= (1 / (a |^ (abs k))) " by Th14
.= ((a |^ (abs k)) ") "
.= (a #Z k) " by A2, Def4
.= 1 / (a #Z k) ;
:: thesis: verum

end;

end;