let D be non empty set ; :: thesis: for f, g being FinSequence of D holds
( len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) & len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) & len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) )
let f, g be FinSequence of D; :: thesis: ( len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) & len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) & len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) )
A1: len (ovlpart (f,g)) <= len g by Def2;
A2: len (ovlcon (f,g)) = (len f) + (len (g /^ (len (ovlpart (f,g))))) by FINSEQ_1:22
.= (len f) + ((len g) -' (len (ovlpart (f,g)))) by RFINSEQ:29
.= (len f) + ((len g) - (len (ovlpart (f,g)))) by A1, XREAL_1:233 ;
hence A3: len (ovlcon (f,g)) = ((len f) + (len g)) - (len (ovlpart (f,g))) ; :: thesis: ( len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) & len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) )
A4: len (ovlpart (f,g)) <= len g by Def2;
hence len (ovlcon (f,g)) = ((len f) + (len g)) -' (len (ovlpart (f,g))) by A3, NAT_1:12, XREAL_1:233; :: thesis: len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g))))
thus len (ovlcon (f,g)) = (len f) + ((len g) -' (len (ovlpart (f,g)))) by A2, A4, XREAL_1:233; :: thesis: verum