let D be non empty set ; :: thesis: for f, g being FinSequence of D st len g = 0 holds
g is_postposition_of f
let f, g be FinSequence of D; :: thesis: ( len g = 0 implies g is_postposition_of f )
assume A1: len g = 0 ; :: thesis: g is_postposition_of f
len (Rev g) = len g by FINSEQ_5:def 3;
then Rev f is_preposition_of by A1, Def8;
hence g is_postposition_of f by Def9; :: thesis: verum