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