let a be real number ; :: thesis: for k being Integer st a <> 0 holds
a #Z (- k) = 1 / (a #Z k)
let k be Integer; :: thesis: ( a <> 0 implies a #Z (- k) = 1 / (a #Z k) )
assume a <> 0 ; :: 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:26;
hence a #Z (- k) = (a |^ (abs (- k))) " by Def4
.= (a |^ (abs k)) " by COMPLEX1:138
.= 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 A4: - k >= 0 ;
a #Z k = (a |^ (abs k)) " by A3, Def4
.= 1 / (a |^ (abs k))
.= 1 / (a |^ (abs (- k))) by COMPLEX1:138
.= 1 / (a #Z (- k)) by A4, Def4 ;
hence a #Z (- k) = 1 / (a #Z k) ; :: thesis: verum

end;

end;