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

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

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

end;

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

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

end;

end;