let a be real number ; :: 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 |^ (abs k) by Def4;
hence a #Z k > 0 by A1, Th13; :: thesis: verum

end;

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

A3: a |^ (abs k) > 0 by A1, Th13;
a #Z k = (a |^ (abs k)) " by A2, Def4;
hence a #Z k > 0 by A3; :: thesis: verum

end;

end;