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 12;
(n + 1) ! = (n + 1) * (n !) by Th15;
hence l divides l ! by A1, NAT_D:def 3; :: thesis: verum