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

now

assume A1: len (ovlpart f,g) > len f ; :: thesis: contradiction
ovlpart f,g = smid f,(((len f) -' (len (ovlpart f,g))) + 1),(len f) by Def2
.= smid f,(0 + 1),(len f) by A1, NAT_2:10
.= f by Th6 ;
hence contradiction by A1; :: thesis: verum

end;

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