let j, l be Nat; :: thesis: ( j <= l & j <> 0 implies j divides l ! )
assume that
A1: j <= l and
A2: j <> 0 ; :: thesis: j divides l !
ex k being Nat st l = j + k by A1, NAT_1:10;
hence j divides l ! by A2, Th40; :: thesis: verum