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

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

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

then reconsider l = l as Element of NAT by INT_1:16;
l >= 0 + 1 by S, NAT_1:13;
then A: 0 |^ l = 0 by NEWTON:16;
abs l = l by ABSVALUE:def 1;
hence 0 #Z l = 0 by A, Def4; :: thesis: verum

end;

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

then reconsider k = - l as Element of NAT by INT_1:16;
k > - 0 by S, XREAL_1:60;
then k >= 0 + 1 by NAT_1:13;
then A: 0 |^ k = 0 by NEWTON:16;
abs l = k by S, ABSVALUE:def 1;
then (0 |^ (abs l)) " = 0 by A;
hence 0 #Z l = 0 by S, Def4; :: thesis: verum

end;

end;