theorem :: FILEREC1:29

for D being non empty set
for f, g being File of D st f is_terminated_by g holds
len g <= len f by FINSEQ_8:def 12;