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, Th6; :: thesis: verum

end;

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

A3: a |^ |.k.| > 0 by A1, Th6;
a #Z k = (a |^ |.k.|) " by A2, Def3;
hence a #Z k > 0 by A3; :: thesis: verum

end;

end;