theorem Th39: :: LIOUVIL1:43

for m, n being non zero Nat holds (Liouville_seq ((seq_const 1),m)) . n = m to_power (- (n !))