theorem Th11: :: IRRAT_1:11

for k being Nat holds (1 / (k + 1)) * (1 / (k !)) = 1 / ((k + 1) !)