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:233;
(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:9;
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:233
.= 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 1
.= 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:58 ;
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:28 ;
hence ovlcon (f,g) = ((f | ((len f) -' (len (ovlpart (f,g))))) ^ (g | (len (ovlpart (f,g))))) ^ (g /^ (len (ovlpart (f,g)))) by A4, RFINSEQ:8
.= (f | ((len f) -' (len (ovlpart (f,g))))) ^ ((g | (len (ovlpart (f,g)))) ^ (g /^ (len (ovlpart (f,g))))) by FINSEQ_1:32
.= (f | ((len f) -' (len (ovlpart (f,g))))) ^ g by RFINSEQ:8 ;
:: thesis: verum