:: deftheorem defines |_ LIOUVIL1:def 1 :
for f being Real_Sequence
for X being Subset of NAT holds f |_ X = (NAT --> 0) +* (f | X);