theorem Th3: :: LIOUVIL1:3

for n being Nat holds n * (n !) = ((n + 1) !) - (n !)