:: deftheorem defines Liouville_constant LIOUVIL1:def 7 :
for a being Real_Sequence
for b being Nat holds Liouville_constant (a,b) = Sum (Liouville_seq (a,b));