let D be non empty set ; :: thesis: for f, g being FinSequence of D holds ovlcon f,g = (f | ((len f) -' (len (ovlpart f,g)))) ^ g
let f, g be FinSequence of D; :: thesis: ovlcon f,g = (f | ((len f) -' (len (ovlpart f,g)))) ^ g
A1: (len f) -' (len (ovlpart f,g)) = (len f) - (len (ovlpart f,g)) by Th10, XREAL_1:235;
(len f) + 1 <= ((len f) + 1) + (len (ovlpart f,g)) by NAT_1:12;
then ((len f) + 1) - (len (ovlpart f,g)) <= (((len f) + 1) + (len (ovlpart f,g))) - (len (ovlpart f,g)) by XREAL_1:11;
then A2: ((len f) + 1) -' (((len f) -' (len (ovlpart f,g))) + 1) = ((len f) + 1) - (((len f) -' (len (ovlpart f,g))) + 1) by A1, XREAL_1:235
.= len (ovlpart f,g) by A1 ;
(len f) -' (len (ovlpart f,g)) <= len f by NAT_D:35;
then A3: len (f /^ ((len f) -' (len (ovlpart f,g)))) = (len f) - ((len f) -' (len (ovlpart f,g))) by RFINSEQ:def 2
.= 0 + (len (ovlpart f,g)) by A1 ;
A4: ovlpart f,g = smid f,(((len f) -' (len (ovlpart f,g))) + 1),(len f) by Def2
.= (f /^ ((len f) -' (len (ovlpart f,g)))) | (len (ovlpart f,g)) by A2, NAT_D:34
.= f /^ ((len f) -' (len (ovlpart f,g))) by A3, FINSEQ_1:79 ;
ovlpart f,g = smid g,1,(len (ovlpart f,g)) by Def2
.= (g /^ ((0 + 1) -' 1)) | (len (ovlpart f,g)) by NAT_D:34
.= (g /^ 0 ) | (len (ovlpart f,g)) by NAT_D:34
.= g | (len (ovlpart f,g)) by FINSEQ_5:31 ;
hence ovlcon f,g = ((f | ((len f) -' (len (ovlpart f,g)))) ^ (g | (len (ovlpart f,g)))) ^ (g /^ (len (ovlpart f,g))) by A4, RFINSEQ:21
.= (f | ((len f) -' (len (ovlpart f,g)))) ^ ((g | (len (ovlpart f,g))) ^ (g /^ (len (ovlpart f,g)))) by FINSEQ_1:45
.= (f | ((len f) -' (len (ovlpart f,g)))) ^ g by RFINSEQ:21 ;
:: thesis: verum