let a be Real; :: 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 ;
hence a #Z (- k) = (a |^ |.(- k).|) " by Def3
.= (a |^ |.k.|) " by COMPLEX1:52
.= 1 / (a |^ |.k.|)
.= 1 / (a #Z k) by A1, Def3 ;
:: thesis: verum

end;

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

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

end;

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

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

end;

end;