let m, n be non zero Nat; :: thesis: (Liouville_seq ((seq_const 1),m)) . n = m to_power (- (n !))
thus (Liouville_seq ((seq_const 1),m)) . n = ((seq_const 1) . n) / (m to_power (n !)) by DefLio
.= 1 / (m to_power (n !)) by SEQ_1:57
.= (1 / m) to_power (n !) by PREPOWER:7
.= m to_power (- (n !)) by POWER:32 ; :: thesis: verum