theorem :: LIOUVIL1:16

for f being Real_Sequence holds f |_ (Seg 0) = seq_const 0