let a be Real; :: thesis: for k being Integer st a <> 0 holds
a #Z k <> 0
let k be Integer; :: thesis: ( a <> 0 implies a #Z k <> 0 )
assume A1: a <> 0 ; :: thesis: a #Z k <> 0

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

suppose k >= 0 ; :: thesis: a #Z k <> 0

then a #Z k = a |^ |.k.| by Def3;
hence a #Z k <> 0 by A1, Th5; :: thesis: verum

end;

suppose k < 0 ; :: thesis: a #Z k <> 0

then a #Z k = (a |^ |.k.|) " by Def3;
hence a #Z k <> 0 by A1, Th5, XCMPLX_1:202; :: thesis: verum

end;

end;