for a being NAT -valued Real_Sequence
for b, n, k being Nat st b > 0 & k <= n holds
((Liouville_seq (a,b)) . k) * ((BLiouville_seq b) . n) is Integer