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 a1: g is_postposition_of f ; :: thesis: len g <= len f
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