let l be Integer; :: thesis: ( l <> 0 implies 0 #Z l = 0 )
assume A1: l <> 0 ; :: thesis: 0 #Z l = 0

per cases ( l > 0 or l < 0 ) by A1;

suppose A2: l > 0 ; :: thesis: 0 #Z l = 0

then reconsider l = l as Element of NAT by INT_1:3;
l >= 0 + 1 by A2, NAT_1:13;
then A3: 0 |^ l = 0 by NEWTON:11;
|.l.| = l by ABSVALUE:def 1;
hence 0 #Z l = 0 by A3, Def3; :: thesis: verum

end;

suppose A4: l < 0 ; :: thesis: 0 #Z l = 0

then reconsider k = - l as Element of NAT by INT_1:3;
k > - 0 by A4;
then k >= 0 + 1 by NAT_1:13;
then A5: 0 |^ k = 0 by NEWTON:11;
|.l.| = k by A4, ABSVALUE:def 1;
then (0 |^ |.l.|) " = 0 by A5;
hence 0 #Z l = 0 by A4, Def3; :: thesis: verum

end;

end;