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

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

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

then - k < - 0 by XREAL_1:24;
hence a #Z (- k) = (a |^ (abs (- k))) " by Def4
.= (a |^ (abs k)) " by COMPLEX1:52
.= 1 / (a |^ (abs k))
.= 1 / (a #Z k) by A1, Def4 ;
:: thesis: verum

end;

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

hence a #Z (- k) = 1 / 1 by Th44
.= 1 / ((a GeoSeq) . 0) by Th4
.= 1 / (a |^ 0) by Def1
.= 1 / (a #Z k) by A2, Th46 ;
:: thesis: verum

end;

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

then a #Z k = (a |^ (abs k)) " by Def4
.= 1 / (a |^ (abs k))
.= 1 / (a |^ (abs (- k))) by COMPLEX1:52
.= 1 / (a #Z (- k)) by A3, Def4 ;
hence a #Z (- k) = 1 / (a #Z k) ; :: thesis: verum

end;

end;