let D be non empty set ; :: thesis: for f, g being FinSequence of D holds len (ovlpart (f,g)) <= len f
let f, g be FinSequence of D; :: thesis: len (ovlpart (f,g)) <= len f

now :: thesis: not len (ovlpart (f,g)) > len f

assume A1: len (ovlpart (f,g)) > len f ; :: thesis: contradiction
then (len f) - (len (ovlpart (f,g))) < 0 by XREAL_1:49;
then (len f) -' (len (ovlpart (f,g))) = 0 by XREAL_0:def 2;
then smid (f,(((len f) -' (len (ovlpart (f,g)))) + 1),(len f)) = f by Th6;
hence contradiction by A1, Def2; :: thesis: verum

end;

hence len (ovlpart (f,g)) <= len f ; :: thesis: verum