:: deftheorem DefLio defines Liouville_seq LIOUVIL1:def 6 :
for a being Real_Sequence
for b being Nat
for b₃ being Real_Sequence holds
( b₃ = Liouville_seq (a,b) iff ( b₃ . 0 = 0 & ( for k being non zero Nat holds b₃ . k = (a . k) / (b to_power (k !)) ) ) );