theorem Th22: :: FINSEQ_8:22
for f, g being FinSequence st len g = 0 holds
g is_postposition_of f