let f, g be FinSequence; :: thesis: ( len g = 0 implies g is_postposition_of f )
assume len g = 0 ; :: thesis: g is_postposition_of f
then Rev g is_preposition_of Rev f by FINSEQ_5:def 3;
hence g is_postposition_of f ; :: thesis: verum