theorem :: FINSEQ_8:28

for D being non empty set
for f being FinSequence of D holds f is_terminated_by f