:: deftheorem LiuSeq defines BLiouville_seq LIOUVIL1:def 8 :
for b being Nat
for b₂ being Real_Sequence holds
( b₂ = BLiouville_seq b iff for n being Nat holds b₂ . n = b to_power (n !) );