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 :: thesis: not len (ovlpart (f,g)) > len f

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:8
.= 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