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

assume A1: len (ovlpart f,g) > len f ; :: thesis: contradiction
then (len f) - (len (ovlpart f,g)) < 0 by XREAL_1:51;
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