let l be Nat; :: thesis: ( l <> 0 implies l divides l ! )
assume l <> 0 ; :: thesis: l divides l !
then consider n being Nat such that
A1: l = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
n + 1 divides (n + 1) !

proof

(n + 1) ! = (n + 1) * (n ! ) by Th21;
hence n + 1 divides (n + 1) ! by NAT_D:def 3; :: thesis: verum

end;

hence l divides l ! by A1; :: thesis: verum