:: deftheorem ALiuDef defines ALiouville_seq LIOUVIL1:def 9 :
for a being Real_Sequence
for b being Nat
for b₃ being Real_Sequence holds
( b₃ = ALiouville_seq (a,b) iff for n being Nat holds b₃ . n = ((BLiouville_seq b) . n) * (Sum ((Liouville_seq (a,b)) |_ (Seg n))) );