for a being Real_Sequence
for n, b being non zero Nat st b > 1 holds
((ALiouville_seq (a,b)) . n) / ((BLiouville_seq b) . n) = Sum (FinSeq ((Liouville_seq (a,b)),n))