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

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