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 ( a = 0 or a > 0 ) by A1;

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

( abs k = 0 or abs k >= 1 ) by NAT_1:14;
then ( (0 |^ (abs k)) " = 0 " or (0 |^ (abs k)) " = 1 " ) by NEWTON:4, NEWTON:11;
hence a #Z k >= 0 by A2, Def4; :: thesis: verum

end;

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

hence a #Z k >= 0 by Th49; :: thesis: verum

end;

end;