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:35
.= (len f) + ((len g) -' (len (ovlpart f,g))) by RFINSEQ:42
.= (len f) + ((len g) - (len (ovlpart f,g))) by A1, XREAL_1:235 ;
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:235; :: 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:235; :: thesis: verum